src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
changeset 39019 e46e7a9cb622
parent 37678 0040bafffdef
child 39028 848be46708dc
equal deleted inserted replaced
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