Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Datatype.ML
changeset 1461 6bcb44e4d6e5
parent 802 2f2fbf0a7e4f
child 6053 8a1059aa01f0 
--- a/src/ZF/Datatype.ML	Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/Datatype.ML	Tue Jan 30 13:42:57 1996 +0100
@@ -26,9 +26,9 @@
 
 signature INDUCTIVE_THMS =
   sig
-  val monos      : thm list		(*monotonicity of each M operator*)
-  val type_intrs : thm list		(*type-checking intro rules*)
-  val type_elims : thm list		(*type-checking elim rules*)
+  val monos      : thm list             (*monotonicity of each M operator*)
+  val type_intrs : thm list             (*type-checking intro rules*)
+  val type_elims : thm list             (*type-checking elim rules*)
   end;
 
 functor Data_section_Fun
@@ -37,7 +37,7 @@
 struct
 
 structure Con = Constructor_Fun 
- 	(structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
+        (structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
 
 structure Inductive = Ind_section_Fun
    (open Arg; 
@@ -55,7 +55,7 @@
 struct
 
 structure Con = Constructor_Fun 
- 	(structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
+        (structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
 
 structure CoInductive = CoInd_section_Fun
    (open Arg;
isabelle