equal
deleted
inserted
replaced
26 ONE_ONE > HOL4Setup.ONE_ONE |
26 ONE_ONE > HOL4Setup.ONE_ONE |
27 ONTO > Fun.surj |
27 ONTO > Fun.surj |
28 TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION |
28 TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION |
29 LET > HOL4Compat.LET; |
29 LET > HOL4Compat.LET; |
30 |
30 |
31 (*ignore_thms |
31 ignore_thms |
32 BOUNDED_DEF |
32 BOUNDED_DEF |
33 BOUNDED_THM |
33 BOUNDED_THM |
34 UNBOUNDED_DEF |
34 UNBOUNDED_DEF |
35 UNBOUNDED_THM; |
35 UNBOUNDED_THM; |
36 *) |
|
37 |
36 |
38 end_import; |
37 end_import; |
39 |
38 |
40 import_theory combin; |
39 import_theory combin; |
41 |
40 |