| changeset 38864 | 4abe644fcea5 |
| parent 38858 | 1920158cfa17 |
| child 38980 | af73cf0dc31f |
| child 39077 | ee78849c1624 |
| 38859:053c69cb4a0e | 38864:4abe644fcea5 |
|---|---|
134 True ~> HOL.True |
134 True ~> HOL.True |
135 False ~> HOL.False |
135 False ~> HOL.False |
136 op & ~> HOL.conj |
136 op & ~> HOL.conj |
137 op | ~> HOL.disj |
137 op | ~> HOL.disj |
138 op --> ~> HOL.implies |
138 op --> ~> HOL.implies |
139 op = ~> HOL.eq |
|
139 Not ~> HOL.Not |
140 Not ~> HOL.Not |
140 The ~> HOL.The |
141 The ~> HOL.The |
141 All ~> HOL.All |
142 All ~> HOL.All |
142 Ex ~> HOL.Ex |
143 Ex ~> HOL.Ex |
143 Ex1 ~> HOL.Ex1 |
144 Ex1 ~> HOL.Ex1 |