]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/tutorial/chapter13.ma
A compiling version
[helm.git] / matita / matita / lib / tutorial / chapter13.ma
index 1971b956ee9421eaac258dadf5c5512253e7032b..c8620fcfd27c478fbd2bf0b92a4883db5bcce6ef 100644 (file)
@@ -3,7 +3,7 @@ Coinductive Types and Predicates
 *)
 
 include "basics/lists/list.ma".
-include "chapter12.ma".
+include "tutorial/chapter12.ma".
 
 (* The only primitive data types of Matita are dependent products and universes.
 So far every other user defined data type has been an inductive type. An