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/ex/listn.ML
changeset 279 7738aed3f84d
parent 85 914270f33f2d 
--- a/src/ZF/ex/listn.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/listn.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -10,14 +10,14 @@
 *)
 
 structure ListN = Inductive_Fun
- (val thy = ListFn.thy addconsts [(["listn"],"i=>i")];
-  val rec_doms = [("listn", "nat*list(A)")];
-  val sintrs = 
-      ["<0,Nil> : listn(A)",
-       "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"];
-  val monos = [];
-  val con_defs = [];
-  val type_intrs = nat_typechecks@List.intrs@[SigmaI]
+ (val thy        = ListFn.thy addconsts [(["listn"],"i=>i")]
+  val rec_doms   = [("listn", "nat*list(A)")]
+  val sintrs     = 
+          ["<0,Nil> : listn(A)",
+           "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
+  val monos      = []
+  val con_defs   = []
+  val type_intrs = nat_typechecks @ List.intrs @ [SigmaI]
   val type_elims = [SigmaE2]);
 
 val listn_induct = standard
isabelle