# HG changeset patch
# User wenzelm
# Date 1191785382 -7200
# Node ID 163c82d039cfdd3b262e0530eaabed3c5292a8d6
# Parent  b8ef7afe3a6b749e4e31fea8d81c9052fbaa91a0
modernized specifications;

diff -r b8ef7afe3a6b -r 163c82d039cf src/ZF/AC/HH.thy
--- 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
 
-
diff -r b8ef7afe3a6b -r 163c82d039cf src/ZF/Induct/Comb.thy
--- 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))"