1.1 --- a/src/HOL/HOL.thy	Tue Oct 07 16:07:14 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Oct 07 16:07:16 2008 +0200
     1.3 @@ -61,7 +61,6 @@
     1.4    Not           :: "bool => bool"                   ("~ _" [40] 40)
     1.5    True          :: bool
     1.6    False         :: bool
     1.7 -  arbitrary     :: 'a
     1.8  
     1.9    The           :: "('a => bool) => 'a"
    1.10    All           :: "('a => bool) => bool"           (binder "ALL " 10)
    1.11 @@ -164,10 +163,8 @@
    1.12  subsubsection {* Axioms and basic definitions *}
    1.13  
    1.14  axioms
    1.15 -  eq_reflection:  "(x=y) ==> (x==y)"
    1.16 -
    1.17    refl:           "t = (t::'a)"
    1.18 -
    1.19 +  subst:          "s = t \<Longrightarrow> P s \<Longrightarrow> P t"
    1.20    ext:            "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
    1.21      -- {*Extensionality is built into the meta-logic, and this rule expresses
    1.22           a related property.  It is an eta-expanded version of the traditional
    1.23 @@ -201,13 +198,15 @@
    1.24    "op ="
    1.25    "op -->"
    1.26    The
    1.27 -  arbitrary
    1.28  
    1.29  axiomatization
    1.30    undefined :: 'a
    1.31  
    1.32 -axiomatization where
    1.33 -  undefined_fun: "undefined x = undefined"
    1.34 +consts
    1.35 +  arbitrary :: 'a
    1.36 +
    1.37 +finalconsts
    1.38 +  arbitrary
    1.39  
    1.40  
    1.41  subsubsection {* Generic classes and algebraic operations *}
    1.42 @@ -304,17 +303,6 @@
    1.43  
    1.44  subsubsection {* Equality *}
    1.45  
    1.46 -text {* Thanks to Stephan Merz *}
    1.47 -lemma subst:
    1.48 -  assumes eq: "s = t" and p: "P s"
    1.49 -  shows "P t"
    1.50 -proof -
    1.51 -  from eq have meta: "s \<equiv> t"
    1.52 -    by (rule eq_reflection)
    1.53 -  from p show ?thesis
    1.54 -    by (unfold meta)
    1.55 -qed
    1.56 -
    1.57  lemma sym: "s = t ==> t = s"
    1.58    by (erule subst) (rule refl)
    1.59  
    1.60 @@ -821,6 +809,9 @@
    1.61  
    1.62  subsubsection {* Atomizing meta-level connectives *}
    1.63  
    1.64 +axiomatization where
    1.65 +  eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" (*admissible axiom*)
    1.66 +
    1.67  lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)"
    1.68  proof
    1.69    assume "!!x. P x"
    1.70 @@ -1681,20 +1672,6 @@
    1.71  
    1.72  subsection {* Code generator basics -- see further theory @{text "Code_Setup"} *}
    1.73  
    1.74 -text {* Module setup *}
    1.75 -
    1.76 -use "~~/src/HOL/Tools/recfun_codegen.ML"
    1.77 -
    1.78 -setup {*
    1.79 -  Code_Name.setup
    1.80 -  #> Code_ML.setup
    1.81 -  #> Code_Haskell.setup
    1.82 -  #> Nbe.setup
    1.83 -  #> Codegen.setup
    1.84 -  #> RecfunCodegen.setup
    1.85 -*}
    1.86 -
    1.87 -
    1.88  text {* Equality *}
    1.89  
    1.90  class eq = type +
    1.91 @@ -1710,6 +1687,19 @@
    1.92  
    1.93  end
    1.94  
    1.95 +text {* Module setup *}
    1.96 +
    1.97 +use "~~/src/HOL/Tools/recfun_codegen.ML"
    1.98 +
    1.99 +setup {*
   1.100 +  Code_Name.setup
   1.101 +  #> Code_ML.setup
   1.102 +  #> Code_Haskell.setup
   1.103 +  #> Nbe.setup
   1.104 +  #> Codegen.setup
   1.105 +  #> RecfunCodegen.setup
   1.106 +*}
   1.107 +
   1.108  
   1.109  subsection {* Legacy tactics and ML bindings *}
   1.110