used ;try assumption instead of .try assumption

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

diff --git a/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma
index b0e94a980c1e776ead4d1c311e84f3a27c59a91e..5b216a3d2bf2cfc9cbd58678218c157cf03a2378 100644 (file)
--- a/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma
@@ -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 lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark))) (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)))) (response (response lark (response (response lark (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.