author wenzelm Sun Apr 15 14:31:44 2007 +0200 (2007-04-15) changeset 22690 0b08f218f260 parent 22689 b800228434a8 child 22691 290454649b8c
replaced axioms/finalconsts by proper axiomatization;
 src/HOL/Hilbert_Choice.thy file | annotate | diff | revisions src/HOL/ZF/HOLZF.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Apr 14 23:56:36 2007 +0200
1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Apr 15 14:31:44 2007 +0200
1.3 @@ -13,8 +13,10 @@
1.4
1.5  subsection {* Hilbert's epsilon *}
1.6
1.7 -consts
1.8 -  Eps           :: "('a => bool) => 'a"
1.9 +axiomatization
1.10 +  Eps :: "('a => bool) => 'a"
1.11 +where
1.12 +  someI: "P x ==> P (Eps P)"
1.13
1.14  syntax (epsilon)
1.15    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
1.16 @@ -23,21 +25,15 @@
1.17  syntax
1.18    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
1.19  translations
1.20 -  "SOME x. P" == "Eps (%x. P)"
1.21 +  "SOME x. P" == "CONST Eps (%x. P)"
1.22
1.23  print_translation {*
1.24  (* to avoid eta-contraction of body *)
1.25 -[("Eps", fn [Abs abs] =>
1.26 +[(@{const_syntax Eps}, fn [Abs abs] =>
1.27       let val (x,t) = atomic_abs_tr' abs
1.28       in Syntax.const "_Eps" \$ x \$ t end)]
1.29  *}
1.30
1.31 -axioms
1.32 -  someI: "P (x::'a) ==> P (SOME x. P x)"
1.33 -finalconsts
1.34 -  Eps
1.35 -
1.36 -
1.37  constdefs
1.38    inv :: "('a => 'b) => ('b => 'a)"
1.39    "inv(f :: 'a => 'b) == %y. SOME x. f x = y"
```
```     2.1 --- a/src/HOL/ZF/HOLZF.thy	Sat Apr 14 23:56:36 2007 +0200
2.2 +++ b/src/HOL/ZF/HOLZF.thy	Sun Apr 15 14:31:44 2007 +0200
2.3 @@ -12,12 +12,12 @@
2.4
2.5  typedecl ZF
2.6
2.7 -consts
2.8 -  Empty :: ZF
2.9 -  Elem :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
2.10 -  Sum :: "ZF \<Rightarrow> ZF"
2.11 -  Power :: "ZF \<Rightarrow> ZF"
2.12 -  Repl :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF"
2.13 +axiomatization
2.14 +  Empty :: ZF and
2.15 +  Elem :: "ZF \<Rightarrow> ZF \<Rightarrow> bool" and
2.16 +  Sum :: "ZF \<Rightarrow> ZF" and
2.17 +  Power :: "ZF \<Rightarrow> ZF" and
2.18 +  Repl :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF" and
2.19    Inf :: ZF
2.20
2.21  constdefs
2.22 @@ -32,9 +32,6 @@
2.23    subset :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
2.24    "subset A B == ! x. Elem x A \<longrightarrow> Elem x B"
2.25
2.26 -finalconsts
2.27 -  Empty Elem Sum Power Repl Inf
2.28 -
2.29  axioms
2.30    Empty: "Not (Elem x Empty)"
2.31    Ext: "(x = y) = (! z. Elem z x = Elem z y)"
```