|
134 | 134 |
|
135 | 135 | - in `boolp.v`: |
136 | 136 | + tactic `eqProp` |
137 | | - + definition `BoolProp` |
| 137 | + + variant `BoolProp` |
138 | 138 | + lemmas `PropB`, `notB`, `andB`, `orB`, `implyB`, `decide_or`, `not_andE`, |
139 | 139 | `not_orE`, `orCA`, `orAC`, `orACA`, `orNp`, `orpN`, `or3E`, `or4E`, `andCA`, |
140 | 140 | `andAC`, `andACA`, `and3E`, `and4E`, `and5E`, `implyNp`, `implypN`, |
|
267 | 267 | `absurd : ident(H)`, `absurd : { hyp_list(Hs) } constr(H)`, |
268 | 268 | `absurd : { hyp_list(Hs) } ident(H)` |
269 | 269 |
|
270 | | - |
271 | | -- in `boolp.v`: |
272 | | - + tactic `eqProp` |
273 | | - + variant `BoolProp` |
274 | | - + lemmas `PropB`, `notB`, `andB`, `orB`, `implyB`, `decide_or`, `not_andE`, |
275 | | - `not_orE`, `orCA`, `orAC`, `orACA`, `orNp`, `orpN`, `or3E`, `or4E`, `andCA`, |
276 | | - `andAC`, `andACA`, `and3E`, `and4E`, `and5E`, `implyNp`, `implypN`, |
277 | | - `implyNN`, `or_andr`, `or_andl`, `and_orr`, `and_orl`, `exists2E`, |
278 | | - `inhabitedE`, `inhabited_witness` |
279 | | - |
280 | 270 | ### Changed |
281 | 271 |
|
282 | 272 | - in `normedtype.v`: |
|
318 | 308 | -in `boolp.v` |
319 | 309 | - lemmas `orC` and `andC` now use `commutative` |
320 | 310 |
|
321 | | --in `boolp.v` |
322 | | - - lemmas `orC` and `andC` now use `commutative` |
323 | | - |
324 | 311 | ### Renamed |
325 | 312 |
|
326 | 313 | - in `exp.v`: |
|
0 commit comments