changeset 39019 | e46e7a9cb622 |
parent 37678 | 0040bafffdef |
child 39028 | 848be46708dc |
39009:95df565aceb7 | 39019:e46e7a9cb622 |
---|---|
52 T > True |
52 T > True |
53 F > False |
53 F > False |
54 ONE_ONE > HOL4Setup.ONE_ONE |
54 ONE_ONE > HOL4Setup.ONE_ONE |
55 ONTO > Fun.surj |
55 ONTO > Fun.surj |
56 "=" > "op =" |
56 "=" > "op =" |
57 "==>" > "op -->" |
57 "==>" > HOL.implies |
58 "/\\" > "op &" |
58 "/\\" > "op &" |
59 "\\/" > "op |" |
59 "\\/" > "op |" |
60 "!" > All |
60 "!" > All |
61 "?" > Ex |
61 "?" > Ex |
62 "?!" > Ex1 |
62 "?!" > Ex1 |