equal
deleted
inserted
replaced
15 |
15 |
16 lemma meta_mp: |
16 lemma meta_mp: |
17 assumes "PROP P ==> PROP Q" and "PROP P" |
17 assumes "PROP P ==> PROP Q" and "PROP P" |
18 shows "PROP Q" |
18 shows "PROP Q" |
19 by (rule `PROP P ==> PROP Q` [OF `PROP P`]) |
19 by (rule `PROP P ==> PROP Q` [OF `PROP P`]) |
|
20 |
|
21 lemmas meta_impE = meta_mp [elim_format] |
20 |
22 |
21 lemma meta_spec: |
23 lemma meta_spec: |
22 assumes "!!x. PROP P(x)" |
24 assumes "!!x. PROP P(x)" |
23 shows "PROP P(x)" |
25 shows "PROP P(x)" |
24 by (rule `!!x. PROP P(x)`) |
26 by (rule `!!x. PROP P(x)`) |