changeset 17628 | f4e2587bc7a5 |
parent 17566 | 484ff733f29c |
child 19233 | 77ca20b0ed77 |
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sat Sep 24 13:54:35 2005 +0200 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sat Sep 24 16:43:41 2005 +0200 @@ -25,7 +25,7 @@ COND > HOL.If bool_case > Datatype.bool.bool_case ONE_ONE > HOL4Setup.ONE_ONE - ONTO > HOL4Setup.ONTO + ONTO > Fun.surj TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION LET > HOL4Compat.LET;