equal
deleted
inserted
replaced
16 that contain !! and ==>, especially in linear scripts. *} |
16 that contain !! and ==>, especially in linear scripts. *} |
17 |
17 |
18 lemma meta_mp: |
18 lemma meta_mp: |
19 assumes major: "PROP P ==> PROP Q" and minor: "PROP P" |
19 assumes major: "PROP P ==> PROP Q" and minor: "PROP P" |
20 shows "PROP Q" |
20 shows "PROP Q" |
21 proof - |
21 by (rule major [OF minor]) |
22 show "PROP Q" by (rule major [OF minor]) |
|
23 qed |
|
24 |
22 |
25 lemma meta_spec: |
23 lemma meta_spec: |
26 assumes major: "!!x. PROP P(x)" |
24 assumes major: "!!x. PROP P(x)" |
27 shows "PROP P(x)" |
25 shows "PROP P(x)" |
28 proof - |
26 by (rule major) |
29 show "PROP P(x)" by (rule major) |
|
30 qed |
|
31 |
27 |
32 lemmas meta_allE = meta_spec [elim_format] |
28 lemmas meta_allE = meta_spec [elim_format] |
33 |
29 |
34 end |
30 end |