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.
Set.insert with authentic syntax
authorhaftmann
Fri, 05 Jun 2009 08:28:24 +0200
changeset 31462 4fcbf17b5a98
parent 31461 d54b743b52a3
child 31463 c5681ed50eab
Set.insert with authentic syntax
src/HOL/Library/LaTeXsugar.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/LaTeXsugar.thy	Fri Jun 05 08:06:03 2009 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jun 05 08:28:24 2009 +0200
@@ -34,7 +34,7 @@
 
 (* insert *)
 translations 
-  "{x} \<union> A" <= "insert x A"
+  "{x} \<union> A" <= "CONST insert x A"
   "{x,y}" <= "{x} \<union> {y}"
   "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
   "{x}" <= "{x} \<union> \<emptyset>"
isabelle