| changeset 58957 | c9e744ea8a38 |
| parent 58889 | 5b7a9633cfa8 |
| child 59498 | 50b60f501b05 |
| 58956:a816aa3ff391 | 58957:c9e744ea8a38 |
|---|---|
132 schematic_lemma cla_rews: |
132 schematic_lemma cla_rews: |
133 "?p1 : P | ~P" |
133 "?p1 : P | ~P" |
134 "?p2 : ~P | P" |
134 "?p2 : ~P | P" |
135 "?p3 : ~ ~ P <-> P" |
135 "?p3 : ~ ~ P <-> P" |
136 "?p4 : (~P --> P) <-> P" |
136 "?p4 : (~P --> P) <-> P" |
137 apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *}) |
137 apply (tactic {* ALLGOALS (Cla.fast_tac @{context} FOLP_cs) *}) |
138 done |
138 done |
139 |
139 |
140 ML_file "simpdata.ML" |
140 ML_file "simpdata.ML" |
141 |
141 |
142 end |
142 end |