new semantics for 'by t'

[helm.git] / helm / software / matita / tests / TPTP / Veloci / COL058-3.p.ma

diff --git a/helm/software/matita/tests/TPTP/Veloci/COL058-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL058-3.p.ma
index 32802b0c56177bcd74497892b06722531bb7103b..b5ed2f6ad3626b26efe8fb9a11d3f58ba4ec3801 100644 (file)
--- a/helm/software/matita/tests/TPTP/Veloci/COL058-3.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL058-3.p.ma
@@ -1,4 +1,4 @@
-set "baseuri" "cic:/matita/TPTP/COL058-3".
+
 include "logic/equality.ma".
 (* Inclusion of: COL058-3.p *)
 (* -------------------------------------------------------------------------- *)
@@ -35,7 +35,7 @@ theorem prove_the_bird_exists:
 \forall H0:\forall X1:Univ.\forall X2:Univ.eq Univ (response (response lark X1) X2) (response X1 (response X2 X2)).eq Univ (response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.