# HG changeset patch
# User wenzelm
# Date 1176640304 -7200
# Node ID 0b08f218f260fd724cd3582c86b0035775844a47
# Parent  b800228434a85bc252e62e366f36ab6e4186fa06
replaced axioms/finalconsts by proper axiomatization;

diff -r b800228434a8 -r 0b08f218f260 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat Apr 14 23:56:36 2007 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sun Apr 15 14:31:44 2007 +0200
@@ -13,8 +13,10 @@
 
 subsection {* Hilbert's epsilon *}
 
-consts
-  Eps           :: "('a => bool) => 'a"
+axiomatization
+  Eps :: "('a => bool) => 'a"
+where
+  someI: "P x ==> P (Eps P)"
 
 syntax (epsilon)
   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
@@ -23,21 +25,15 @@
 syntax
   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
 translations
-  "SOME x. P" == "Eps (%x. P)"
+  "SOME x. P" == "CONST Eps (%x. P)"
 
 print_translation {*
 (* to avoid eta-contraction of body *)
-[("Eps", fn [Abs abs] =>
+[(@{const_syntax Eps}, fn [Abs abs] =>
      let val (x,t) = atomic_abs_tr' abs
      in Syntax.const "_Eps" $ x $ t end)]
 *}
 
-axioms
-  someI: "P (x::'a) ==> P (SOME x. P x)"
-finalconsts
-  Eps
-
-
 constdefs
   inv :: "('a => 'b) => ('b => 'a)"
   "inv(f :: 'a => 'b) == %y. SOME x. f x = y"
diff -r b800228434a8 -r 0b08f218f260 src/HOL/ZF/HOLZF.thy
--- a/src/HOL/ZF/HOLZF.thy	Sat Apr 14 23:56:36 2007 +0200
+++ b/src/HOL/ZF/HOLZF.thy	Sun Apr 15 14:31:44 2007 +0200
@@ -12,12 +12,12 @@
 
 typedecl ZF
 
-consts
-  Empty :: ZF
-  Elem :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
-  Sum :: "ZF \<Rightarrow> ZF"
-  Power :: "ZF \<Rightarrow> ZF"
-  Repl :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF"
+axiomatization
+  Empty :: ZF and
+  Elem :: "ZF \<Rightarrow> ZF \<Rightarrow> bool" and
+  Sum :: "ZF \<Rightarrow> ZF" and
+  Power :: "ZF \<Rightarrow> ZF" and
+  Repl :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF" and
   Inf :: ZF
 
 constdefs
@@ -32,9 +32,6 @@
   subset :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
   "subset A B == ! x. Elem x A \<longrightarrow> Elem x B"
 
-finalconsts 
-  Empty Elem Sum Power Repl Inf
-
 axioms
   Empty: "Not (Elem x Empty)"
   Ext: "(x = y) = (! z. Elem z x = Elem z y)"