equal
deleted
inserted
replaced
10 To generate similar output to manual, execute these commands: |
10 To generate similar output to manual, execute these commands: |
11 Pretty.setmargin 72; print_depth 0; |
11 Pretty.setmargin 72; print_depth 0; |
12 *) |
12 *) |
13 |
13 |
14 |
14 |
15 (**** Some simple backward proofs ****) |
15 (**** SOME simple backward proofs ****) |
16 |
16 |
17 goal FOLP.thy "?p:P|P --> P"; |
17 goal FOLP.thy "?p:P|P --> P"; |
18 by (rtac impI 1); |
18 by (rtac impI 1); |
19 by (rtac disjE 1); |
19 by (rtac disjE 1); |
20 by (assume_tac 3); |
20 by (assume_tac 3); |