# HG changeset patch
# User wenzelm
# Date 876402186 -7200
# Node ID 46b255e140dc9b9b5a2ac9cb2468a3614dc78319
# Parent  5a6a6f18b109ec115c64c46eb20d37bd6dfdb795
fixed infix syntax;

diff -r 5a6a6f18b109 -r 46b255e140dc src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Oct 09 15:01:11 1997 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 09 15:03:06 1997 +0200
@@ -25,10 +25,6 @@
   bool :: term
 
 
-syntax ("" output)
-  "op ="        :: ['a, 'a] => bool                 ("(_ =/ _)" [51, 51] 50)
-  "op ~="       :: ['a, 'a] => bool                 ("(_ ~=/ _)" [51, 51] 50)
-
 consts
 
   (* Constants *)
@@ -75,6 +71,7 @@
   "*"           :: ['a::times, 'a] => 'a            (infixl 70)
   (*See Nat.thy for "^"*)
 
+
 (** Additional concrete syntax **)
 
 types
@@ -116,11 +113,9 @@
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   "let x = a in e"        == "Let a (%x. e)"
 
-syntax (symbols output)
-  "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
-  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
-  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
-  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
+syntax ("" output)
+  "op ="        :: ['a, 'a] => bool                 ("(_ =/ _)" [51, 51] 50)
+  "op ~="       :: ['a, 'a] => bool                 ("(_ ~=/ _)" [51, 51] 50)
 
 syntax (symbols)
   Not           :: bool => bool                     ("\\<not> _" [40] 40)
@@ -136,6 +131,12 @@
   "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
 (*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
 
+syntax (symbols output)
+  "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
+  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
+  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
+  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
+
 
 
 (** Rules and definitions **)
@@ -178,8 +179,9 @@
   o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
   if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
 
-constdefs arbitrary :: 'a
-         "arbitrary == @x.False"
+consts
+  arbitrary :: 'a
+
 
 end
 
diff -r 5a6a6f18b109 -r 46b255e140dc src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Thu Oct 09 15:01:11 1997 +0200
+++ b/src/HOL/Ord.thy	Thu Oct 09 15:03:06 1997 +0200
@@ -11,6 +11,10 @@
 axclass
   ord < term
 
+syntax
+  "op <"        :: ['a::ord, 'a] => bool             ("op <")
+  "op <="       :: ['a::ord, 'a] => bool             ("op <=")
+
 consts
   "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50, 51] 50)
   "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50, 51] 50)
@@ -19,13 +23,10 @@
 
   Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
 
-syntax
-  "op <"        :: ['a::ord, 'a] => bool             ("op <")
-  "op <="       :: ['a::ord, 'a] => bool             ("op <=")
+syntax (symbols)
+  "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
+  "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
 
-syntax (symbols)
-  "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
-  "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
 
 defs
   mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
diff -r 5a6a6f18b109 -r 46b255e140dc src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Oct 09 15:01:11 1997 +0200
+++ b/src/HOL/Set.thy	Thu Oct 09 15:03:06 1997 +0200
@@ -18,6 +18,9 @@
 instance
   set :: (term) {ord, minus, power}
 
+syntax
+  "op :"        :: ['a, 'a set] => bool             ("op :")
+
 consts
   "{}"          :: 'a set                           ("{}")
   insert        :: ['a, 'a set] => 'a set
@@ -42,14 +45,12 @@
 
 syntax
 
-  "op :"        :: ['a, 'a set] => bool               ("op :")
-
   UNIV          :: 'a set
 
   (* Infix syntax for non-membership *)
 
+  "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
   "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
-  "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
 
   "@Finset"     :: args => 'a set                     ("{(_)}")
 
@@ -83,22 +84,22 @@
   "EX x:A. P"   => "Bex A (%x. P)"
 
 syntax ("" output)
+  "_setle"      :: ['a set, 'a set] => bool           ("op <=")
   "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
-  "_setle"      :: ['a set, 'a set] => bool           ("op <=")
+  "_setless"    :: ['a set, 'a set] => bool           ("op <")
   "_setless"    :: ['a set, 'a set] => bool           ("(_/ < _)" [50, 51] 50)
-  "_setless"    :: ['a set, 'a set] => bool           ("op <")
 
 syntax (symbols)
+  "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
   "_setle"      :: ['a set, 'a set] => bool           ("(_/ \\<subseteq> _)" [50, 51] 50)
-  "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
+  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
   "_setless"    :: ['a set, 'a set] => bool           ("(_/ \\<subset> _)" [50, 51] 50)
-  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
   "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
   "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
+  "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
   "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
-  "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
+  "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
   "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
-  "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
   "UN "         :: [idts, bool] => bool               ("(3\\<Union> _./ _)" 10)
   "INT "        :: [idts, bool] => bool               ("(3\\<Inter> _./ _)" 10)
   "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union> _\\<in>_./ _)" 10)