changeset 13328 | 703de709a64b |
parent 13269 | 3ba9be497c33 |
child 13356 | c9cfe1638bf2 |
--- a/src/ZF/Epsilon.thy Tue Jul 09 23:03:21 2002 +0200 +++ b/src/ZF/Epsilon.thy Tue Jul 09 23:05:26 2002 +0200 @@ -3,9 +3,10 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Epsilon induction and recursion *) +header{*Epsilon Induction and Recursion*} + theory Epsilon = Nat + mono: constdefs