]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/tests/bool.ma
New syntax and semantics for the rewriting steps that make the pretty-printed
[helm.git] / helm / software / matita / tests / bool.ma
index 6abd2cbb1dcc4be7516409972abe7ff796085bc3..2b7f815b98afb95e5fb19c90ffe2e6b85a1b52a5 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/SK/".
+set "baseuri" "cic:/matita/tests/bool/".
 
 include "legacy/coq.ma".
 
@@ -629,5 +629,5 @@ theorem bool5:
 intros.auto paramodulation.
 qed.
 
-*)
+*)*)