1.1 --- a/src/HOL/HOL.thy	Fri Mar 16 22:22:05 2012 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Mar 16 22:31:19 2012 +0100
     1.3 @@ -57,6 +57,11 @@
     1.4  judgment
     1.5    Trueprop      :: "bool => prop"                   ("(_)" 5)
     1.6  
     1.7 +axiomatization
     1.8 +  implies       :: "[bool, bool] => bool"           (infixr "-->" 25)  and
     1.9 +  eq            :: "['a, 'a] => bool"               (infixl "=" 50)  and
    1.10 +  The           :: "('a => bool) => 'a"
    1.11 +
    1.12  consts
    1.13    True          :: bool
    1.14    False         :: bool
    1.15 @@ -64,11 +69,7 @@
    1.16  
    1.17    conj          :: "[bool, bool] => bool"           (infixr "&" 35)
    1.18    disj          :: "[bool, bool] => bool"           (infixr "|" 30)
    1.19 -  implies       :: "[bool, bool] => bool"           (infixr "-->" 25)
    1.20  
    1.21 -  eq            :: "['a, 'a] => bool"               (infixl "=" 50)
    1.22 -
    1.23 -  The           :: "('a => bool) => 'a"
    1.24    All           :: "('a => bool) => bool"           (binder "ALL " 10)
    1.25    Ex            :: "('a => bool) => bool"           (binder "EX " 10)
    1.26    Ex1           :: "('a => bool) => bool"           (binder "EX! " 10)
    1.27 @@ -106,10 +107,8 @@
    1.28  notation (xsymbols)
    1.29    iff  (infixr "\<longleftrightarrow>" 25)
    1.30  
    1.31 -syntax
    1.32 -  "_The" :: "[pttrn, bool] => 'a"  ("(3THE _./ _)" [0, 10] 10)
    1.33 -translations
    1.34 -  "THE x. P" == "CONST The (%x. P)"
    1.35 +syntax "_The" :: "[pttrn, bool] => 'a"  ("(3THE _./ _)" [0, 10] 10)
    1.36 +translations "THE x. P" == "CONST The (%x. P)"
    1.37  print_translation {*
    1.38    [(@{const_syntax The}, fn [Abs abs] =>
    1.39        let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    1.40 @@ -150,19 +149,22 @@
    1.41  
    1.42  subsubsection {* Axioms and basic definitions *}
    1.43  
    1.44 -axioms
    1.45 -  refl:           "t = (t::'a)"
    1.46 -  subst:          "s = t \<Longrightarrow> P s \<Longrightarrow> P t"
    1.47 -  ext:            "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
    1.48 +axiomatization where
    1.49 +  refl: "t = (t::'a)" and
    1.50 +  subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
    1.51 +  ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
    1.52      -- {*Extensionality is built into the meta-logic, and this rule expresses
    1.53           a related property.  It is an eta-expanded version of the traditional
    1.54 -         rule, and similar to the ABS rule of HOL*}
    1.55 +         rule, and similar to the ABS rule of HOL*} and
    1.56  
    1.57    the_eq_trivial: "(THE x. x = a) = (a::'a)"
    1.58  
    1.59 -  impI:           "(P ==> Q) ==> P-->Q"
    1.60 -  mp:             "[| P-->Q;  P |] ==> Q"
    1.61 +axiomatization where
    1.62 +  impI: "(P ==> Q) ==> P-->Q" and
    1.63 +  mp: "[| P-->Q;  P |] ==> Q" and
    1.64  
    1.65 +  iff: "(P-->Q) --> (Q-->P) --> (P=Q)" and
    1.66 +  True_or_False: "(P=True) | (P=False)"
    1.67  
    1.68  defs
    1.69    True_def:     "True      == ((%x::bool. x) = (%x. x))"
    1.70 @@ -174,30 +176,19 @@
    1.71    or_def:       "P | Q     == !R. (P-->R) --> (Q-->R) --> R"
    1.72    Ex1_def:      "Ex1(P)    == ? x. P(x) & (! y. P(y) --> y=x)"
    1.73  
    1.74 -axioms
    1.75 -  iff:          "(P-->Q) --> (Q-->P) --> (P=Q)"
    1.76 -  True_or_False:  "(P=True) | (P=False)"
    1.77 +definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
    1.78 +  where "If P x y \<equiv> (THE z::'a. (P=True --> z=x) & (P=False --> z=y))"
    1.79  
    1.80 -finalconsts
    1.81 -  eq
    1.82 -  implies
    1.83 -  The
    1.84 -
    1.85 -definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
    1.86 -  "If P x y \<equiv> (THE z::'a. (P=True --> z=x) & (P=False --> z=y))"
    1.87 -
    1.88 -definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" where
    1.89 -  "Let s f \<equiv> f s"
    1.90 +definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
    1.91 +  where "Let s f \<equiv> f s"
    1.92  
    1.93  translations
    1.94    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
    1.95    "let x = a in e"        == "CONST Let a (%x. e)"
    1.96  
    1.97 -axiomatization
    1.98 -  undefined :: 'a
    1.99 +axiomatization undefined :: 'a
   1.100  
   1.101 -class default =
   1.102 -  fixes default :: 'a
   1.103 +class default = fixes default :: 'a
   1.104  
   1.105  
   1.106  subsection {* Fundamental rules *}