--- 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 *}