equal
deleted
inserted
replaced
22 assumes "!!x. PROP P(x)" |
22 assumes "!!x. PROP P(x)" |
23 shows "PROP P(x)" |
23 shows "PROP P(x)" |
24 by (rule `!!x. PROP P(x)`) |
24 by (rule `!!x. PROP P(x)`) |
25 |
25 |
26 lemmas meta_allE = meta_spec [elim_format] |
26 lemmas meta_allE = meta_spec [elim_format] |
|
27 |
|
28 |
|
29 subsection {* Embedded terms *} |
|
30 |
|
31 locale (open) meta_term_syntax = |
|
32 fixes meta_term :: "'a => prop" ("TERM _") |
|
33 |
|
34 parse_translation {* |
|
35 [("\<^fixed>meta_term", fn [t] => Logic.mk_term t)] |
|
36 *} |
|
37 |
|
38 lemmas [intro?] = termI |
27 |
39 |
28 |
40 |
29 subsection {* Meta-level conjunction *} |
41 subsection {* Meta-level conjunction *} |
30 |
42 |
31 locale (open) meta_conjunction_syntax = |
43 locale (open) meta_conjunction_syntax = |