equal
deleted
inserted
replaced
1290 -- {* Miniscoping: pushing in universal quantifiers. *} |
1290 -- {* Miniscoping: pushing in universal quantifiers. *} |
1291 by (iprover | blast)+ |
1291 by (iprover | blast)+ |
1292 |
1292 |
1293 lemmas [simp] = |
1293 lemmas [simp] = |
1294 triv_forall_equality (*prunes params*) |
1294 triv_forall_equality (*prunes params*) |
1295 True_implies_equals (*prune asms `True'*) |
1295 True_implies_equals implies_True_equals (*prune True in asms*) |
|
1296 False_implies_equals (*prune False in asms*) |
1296 if_True |
1297 if_True |
1297 if_False |
1298 if_False |
1298 if_cancel |
1299 if_cancel |
1299 if_eq_cancel |
1300 if_eq_cancel |
1300 imp_disjL |
1301 imp_disjL |