Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add space to binder syntax
authorhuffman
Fri, 18 Jan 2008 20:34:28 +0100
changeset 25927 9c544dac6269
parent 25926 aa0eca1ccb19
child 25928 042e877d9841
add space to binder syntax
src/HOLCF/Cfun.thy file | annotate | diff | comparison | revisions
src/HOLCF/Fix.thy file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Cfun.thy	Fri Jan 18 20:31:11 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Fri Jan 18 20:34:28 2008 +0100
@@ -68,7 +68,7 @@
   "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic"  ("(3LAM _./ _)" [1000, 10] 10)
 
 syntax (xsymbols)
-  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda>_./ _)" [1000, 10] 10)
+  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
 
 parse_ast_translation {*
 (* rewrites (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
--- a/src/HOLCF/Fix.thy	Fri Jan 18 20:31:11 2008 +0100
+++ b/src/HOLCF/Fix.thy	Fri Jan 18 20:34:28 2008 +0100
@@ -59,7 +59,7 @@
   "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3FIX _./ _)" [1000, 10] 10)
 
 syntax (xsymbols)
-  "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu>_./ _)" [1000, 10] 10)
+  "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu> _./ _)" [1000, 10] 10)
 
 translations
   "\<mu> x. t" == "CONST fix\<cdot>(\<Lambda> x. t)"
isabelle