--- a/src/ZF/AC/HH.thy Sun Oct 07 21:19:31 2007 +0200
+++ b/src/ZF/AC/HH.thy Sun Oct 07 21:29:42 2007 +0200
@@ -10,9 +10,8 @@
theory HH imports AC_Equiv Hartog begin
-constdefs
-
- HH :: "[i, i, i] => i"
+definition
+ HH :: "[i, i, i] => i" where
"HH(f,x,a) == transrec(a, %b r. let z = x - (\<Union>c \<in> b. r`c)
in if f`z \<in> Pow(z)-{0} then f`z else {x})"
@@ -243,4 +242,3 @@
end
-
--- a/src/ZF/Induct/Comb.thy Sun Oct 07 21:19:31 2007 +0200
+++ b/src/ZF/Induct/Comb.thy Sun Oct 07 21:29:42 2007 +0200
@@ -77,11 +77,12 @@
Misc definitions.
*}
-constdefs
- I :: i
+definition
+ I :: i where
"I == S\<bullet>K\<bullet>K"
- diamond :: "i => o"
+definition
+ diamond :: "i => o" where
"diamond(r) ==
\<forall>x y. <x,y>\<in>r --> (\<forall>y'. <x,y'>\<in>r --> (\<exists>z. <y,z>\<in>r & <y',z> \<in> r))"