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.
xsymbols for {| and |}
authorpaulson
Thu, 24 Aug 2000 12:39:42 +0200
changeset 9686 87b460d72e80
parent 9685 6d123a7e30bd
child 9687 772ac061bd76
xsymbols for {| and |}
src/HOL/Auth/Message.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Auth/Message.thy	Thu Aug 24 12:39:24 2000 +0200
+++ b/src/HOL/Auth/Message.thy	Thu Aug 24 12:39:42 2000 +0200
@@ -42,6 +42,9 @@
 syntax
   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
 
+syntax (xsymbols)
+  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\\<lbrace>_,/ _\\<rbrace>)")
+
 translations
   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
   "{|x, y|}"      == "MPair x y"
isabelle