]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/tests/record.ma
version 0.7.1
[helm.git] / helm / matita / tests / record.ma
index 61dec1d7e34671c1ca7a1d890b10f789ab43bec0..02ef85a0504ddd2c939b2a69ffe752bc544caedd 100644 (file)
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/matita/tests/record/".
+
 record empty : Type \def {}.
 
 inductive True : Prop \def I: True.
@@ -20,4 +22,4 @@ record paperino: Prop \def {
   paolo : Type;
   pippo : paolo \to paolo;
   piero : True
-}.
\ No newline at end of file
+}.