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/HOL/Library/OptionalSugar.thy
changeset 35250 92664dca6f20
parent 35115 446c5063e4fd
child 38864 4abe644fcea5 
--- a/src/HOL/Library/OptionalSugar.thy	Sat Feb 20 23:23:04 2010 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Sun Feb 21 20:53:50 2010 +0100
@@ -37,15 +37,15 @@
 
 (* Let *)
 translations 
-  "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
-  "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"
+  "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)"
+  "_bind (CONST DUMMY, p) e" <= "_bind p (CONST snd e)"
 
   "_tuple_args x (_tuple_args y z)" ==
     "_tuple_args x (_tuple_arg (_tuple y z))"
 
-  "_bind (Some p) e" <= "_bind p (CONST the e)"
-  "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
-  "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
+  "_bind (CONST Some p) e" <= "_bind p (CONST the e)"
+  "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
+  "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
 
 (* type constraints with spacing *)
 setup {*
isabelle