| changeset 38795 | 848be46708dc |
| parent 38786 | e46e7a9cb622 |
| child 38864 | 4abe644fcea5 |
| 38794:2d638e963357 | 38795:848be46708dc |
|---|---|
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 "==>" > HOL.implies |
57 "==>" > HOL.implies |
58 "/\\" > "op &" |
58 "/\\" > HOL.conj |
59 "\\/" > "op |" |
59 "\\/" > HOL.disj |
60 "!" > All |
60 "!" > All |
61 "?" > Ex |
61 "?" > Ex |
62 "?!" > Ex1 |
62 "?!" > Ex1 |
63 "~" > Not |
63 "~" > Not |
64 o > Fun.comp |
64 o > Fun.comp |