--- a/src/ZF/AC/HH.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/HH.thy Fri Jul 25 07:35:53 2008 +0200
@@ -8,7 +8,9 @@
AC15 ==> WO6
*)
-theory HH imports AC_Equiv Hartog begin
+theory HH
+imports AC_Equiv Hartog
+begin
definition
HH :: "[i, i, i] => i" where