# HG changeset patch
# User haftmann
# Date 1223388436 -7200
# Node ID b0b30fd6c264d9a2c65117ab5170cd408fe61258
# Parent  f29fecd6ddaac7c63946ff90278a675bc2cc694c
re-introduces axiom subst

diff -r f29fecd6ddaa -r b0b30fd6c264 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Oct 07 16:07:14 2008 +0200
+++ b/src/HOL/HOL.thy	Tue Oct 07 16:07:16 2008 +0200
@@ -61,7 +61,6 @@
   Not           :: "bool => bool"                   ("~ _" [40] 40)
   True          :: bool
   False         :: bool
-  arbitrary     :: 'a
 
   The           :: "('a => bool) => 'a"
   All           :: "('a => bool) => bool"           (binder "ALL " 10)
@@ -164,10 +163,8 @@
 subsubsection {* Axioms and basic definitions *}
 
 axioms
-  eq_reflection:  "(x=y) ==> (x==y)"
-
   refl:           "t = (t::'a)"
-
+  subst:          "s = t \<Longrightarrow> P s \<Longrightarrow> P t"
   ext:            "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
     -- {*Extensionality is built into the meta-logic, and this rule expresses
          a related property.  It is an eta-expanded version of the traditional
@@ -201,13 +198,15 @@
   "op ="
   "op -->"
   The
-  arbitrary
 
 axiomatization
   undefined :: 'a
 
-axiomatization where
-  undefined_fun: "undefined x = undefined"
+consts
+  arbitrary :: 'a
+
+finalconsts
+  arbitrary
 
 
 subsubsection {* Generic classes and algebraic operations *}
@@ -304,17 +303,6 @@
 
 subsubsection {* Equality *}
 
-text {* Thanks to Stephan Merz *}
-lemma subst:
-  assumes eq: "s = t" and p: "P s"
-  shows "P t"
-proof -
-  from eq have meta: "s \<equiv> t"
-    by (rule eq_reflection)
-  from p show ?thesis
-    by (unfold meta)
-qed
-
 lemma sym: "s = t ==> t = s"
   by (erule subst) (rule refl)
 
@@ -821,6 +809,9 @@
 
 subsubsection {* Atomizing meta-level connectives *}
 
+axiomatization where
+  eq_reflection: "x = y \<Longrightarrow> x \<equiv> y" (*admissible axiom*)
+
 lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)"
 proof
   assume "!!x. P x"
@@ -1681,20 +1672,6 @@
 
 subsection {* Code generator basics -- see further theory @{text "Code_Setup"} *}
 
-text {* Module setup *}
-
-use "~~/src/HOL/Tools/recfun_codegen.ML"
-
-setup {*
-  Code_Name.setup
-  #> Code_ML.setup
-  #> Code_Haskell.setup
-  #> Nbe.setup
-  #> Codegen.setup
-  #> RecfunCodegen.setup
-*}
-
-
 text {* Equality *}
 
 class eq = type +
@@ -1710,6 +1687,19 @@
 
 end
 
+text {* Module setup *}
+
+use "~~/src/HOL/Tools/recfun_codegen.ML"
+
+setup {*
+  Code_Name.setup
+  #> Code_ML.setup
+  #> Code_Haskell.setup
+  #> Nbe.setup
+  #> Codegen.setup
+  #> RecfunCodegen.setup
+*}
+
 
 subsection {* Legacy tactics and ML bindings *}