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 30404 d03dd6301678
parent 29494 a189c6274c7a
child 30474 52e92009aacb 
--- a/src/HOL/Library/OptionalSugar.thy	Mon Mar 09 23:07:51 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Tue Mar 10 10:59:59 2009 +0100
@@ -9,7 +9,7 @@
 
 (* set *)
 translations
-  "xs" <= "set xs"
+  "xs" <= "CONST set xs"
 
 (* append *)
 syntax (latex output)
@@ -26,15 +26,15 @@
 
 (* Let *)
 translations 
-  "_bind (p,DUMMY) e" <= "_bind p (fst e)"
-  "_bind (DUMMY,p) e" <= "_bind p (snd e)"
+  "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
+  "_bind (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 (the e)"
-  "_bind (p#DUMMY) e" <= "_bind p (hd e)"
-  "_bind (DUMMY#p) e" <= "_bind p (tl e)"
+  "_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)"
 
 (* type constraints with spacing *)
 setup {*
isabelle