--- a/src/ZF/epsilon.thy Tue Nov 16 14:23:19 1993 +0100
+++ b/src/ZF/epsilon.thy Tue Nov 16 14:24:21 1993 +0100
@@ -6,7 +6,7 @@
Epsilon induction and recursion
*)
-Epsilon = Nat +
+Epsilon = Nat + "mono" +
consts
eclose,rank :: "i=>i"
transrec :: "[i, [i,i]=>i] =>i"