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/Resid/Terms.thy
changeset 11319 8b84ee2cc79c
parent 6046 2c8a8be36c94 
--- a/src/ZF/Resid/Terms.thy	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Terms.thy	Mon May 21 14:51:46 2001 +0200
@@ -18,9 +18,9 @@
 inductive
   domains       "lambda" <= "redexes"
   intrs
-    Lambda_Var  "               n:nat ==>     Var(n):lambda"
-    Lambda_Fun  "            u:lambda ==>     Fun(u):lambda"
-    Lambda_App  "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
+    Lambda_Var  "               n \\<in> nat ==>     Var(n):lambda"
+    Lambda_Fun  "            u \\<in> lambda ==>     Fun(u):lambda"
+    Lambda_App  "[|u \\<in> lambda; v \\<in> lambda|]==> Apl(u,v):lambda"
   type_intrs    "redexes.intrs@bool_typechecks"
 
 primrec
isabelle