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.
tuned ``syntax (output)'';
authorwenzelm
Fri, 04 Jan 2002 19:29:30 +0100
changeset 12633 ad9277743664
parent 12632 3d3e356778b5
child 12634 3baa6143a9c4
tuned ``syntax (output)'';
src/HOL/HOL.thy file | annotate | diff | comparison | revisions
src/HOL/Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL.thy	Fri Jan 04 19:28:57 2002 +0100
+++ b/src/HOL/HOL.thy	Fri Jan 04 19:29:30 2002 +0100
@@ -75,7 +75,7 @@
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   "let x = a in e"        == "Let a (%x. e)"
 
-syntax ("" output)
+syntax (output)
   "="           :: "['a, 'a] => bool"                    (infix 50)
   "~="          :: "['a, 'a] => bool"                    (infix 50)
 
--- a/src/HOL/Set.thy	Fri Jan 04 19:28:57 2002 +0100
+++ b/src/HOL/Set.thy	Fri Jan 04 19:29:30 2002 +0100
@@ -85,7 +85,7 @@
   "ALL x:A. P"  == "Ball A (%x. P)"
   "EX x:A. P"   == "Bex A (%x. P)"
 
-syntax ("" output)
+syntax (output)
   "_setle"      :: "'a set => 'a set => bool"             ("op <=")
   "_setle"      :: "'a set => 'a set => bool"             ("(_/ <= _)" [50, 51] 50)
   "_setless"    :: "'a set => 'a set => bool"             ("op <")
isabelle