tuned ``syntax (output)'';
authorwenzelm
Fri Jan 04 19:29:30 2002 +0100 (2002-01-04)
changeset 12633ad9277743664
parent 12632 3d3e356778b5
child 12634 3baa6143a9c4
tuned ``syntax (output)'';
src/HOL/HOL.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.thy	Fri Jan 04 19:28:57 2002 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Jan 04 19:29:30 2002 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
     1.5    "let x = a in e"        == "Let a (%x. e)"
     1.6  
     1.7 -syntax ("" output)
     1.8 +syntax (output)
     1.9    "="           :: "['a, 'a] => bool"                    (infix 50)
    1.10    "~="          :: "['a, 'a] => bool"                    (infix 50)
    1.11  
     2.1 --- a/src/HOL/Set.thy	Fri Jan 04 19:28:57 2002 +0100
     2.2 +++ b/src/HOL/Set.thy	Fri Jan 04 19:29:30 2002 +0100
     2.3 @@ -85,7 +85,7 @@
     2.4    "ALL x:A. P"  == "Ball A (%x. P)"
     2.5    "EX x:A. P"   == "Bex A (%x. P)"
     2.6  
     2.7 -syntax ("" output)
     2.8 +syntax (output)
     2.9    "_setle"      :: "'a set => 'a set => bool"             ("op <=")
    2.10    "_setle"      :: "'a set => 'a set => bool"             ("(_/ <= _)" [50, 51] 50)
    2.11    "_setless"    :: "'a set => 'a set => bool"             ("op <")