]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/tests/bool.ma
An idea to implement manifest record fields:
[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.
 
-*)
+*)*)