--- 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)"