| changeset 15531 | 08c8dad8e399 |
| parent 5204 | 858da18069d7 |
| child 15661 | 9ef583b08647 |
| 15530:6f43714517ee | 15531:08c8dad8e399 |
|---|---|
12 *) |
12 *) |
13 |
13 |
14 |
14 |
15 context FOL.thy; |
15 context FOL.thy; |
16 |
16 |
17 (**** Some simple backward proofs ****) |
17 (**** SOME simple backward proofs ****) |
18 |
18 |
19 Goal "P|P --> P"; |
19 Goal "P|P --> P"; |
20 by (rtac impI 1); |
20 by (rtac impI 1); |
21 by (rtac disjE 1); |
21 by (rtac disjE 1); |
22 by (assume_tac 3); |
22 by (assume_tac 3); |