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/llist_eq.ML
changeset 279 7738aed3f84d
parent 173 85071e6ad295 
--- a/src/ZF/ex/llist_eq.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/llist_eq.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -11,14 +11,14 @@
   a q/Q to the Sigma, Pair and converse rules.*)
 
 structure LList_Eq = CoInductive_Fun
- (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
-  val rec_doms = [("lleq", "llist(A) * llist(A)")];
-  val sintrs = 
-      ["<LNil, LNil> : lleq(A)",
-       "[| a:A;  <l, l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')> : lleq(A)"];
-  val monos = [];
-  val con_defs = [];
-  val type_intrs = LList.intrs@[SigmaI];
+ (val thy = LList.thy addconsts [(["lleq"],"i=>i")]
+  val rec_doms   = [("lleq", "llist(A) * llist(A)")]
+  val sintrs     = 
+        ["<LNil, LNil> : lleq(A)",
+         "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"]
+  val monos      = []
+  val con_defs   = []
+  val type_intrs = LList.intrs @ [SigmaI]
   val type_elims = [SigmaE2]);
 
 (** Alternatives for above:
isabelle