src/HOL/HOL.thy

 
 arities
   fun :: (term, term) term
   bool :: term
 
-
-syntax ("" output)
-  "op ="        :: ['a, 'a] => bool                 ("(_ =/ _)" [51, 51] 50)
-  "op ~="       :: ['a, 'a] => bool                 ("(_ ~=/ _)" [51, 51] 50)
 
 consts
 
   (* Constants *)
 

 consts
   "+"           :: ['a::plus, 'a]  => 'a            (infixl 65)
   "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
   "*"           :: ['a::times, 'a] => 'a            (infixl 70)
   (*See Nat.thy for "^"*)
+
 
 (** Additional concrete syntax **)
 
 types
   letbinds  letbind

   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
   "_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)
   "op &"        :: [bool, bool] => bool             (infixr "\\<and>" 35)
   "op |"        :: [bool, bool] => bool             (infixr "\\<or>" 30)

   "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
   "@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 **)
 
 rules

 
   Let_def       "Let s f == f(s)"
   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
 
 
 ML