equal
deleted
inserted
replaced
31 subsection {* Embedded terms *} |
31 subsection {* Embedded terms *} |
32 |
32 |
33 locale (open) meta_term_syntax = |
33 locale (open) meta_term_syntax = |
34 fixes meta_term :: "'a => prop" ("TERM _") |
34 fixes meta_term :: "'a => prop" ("TERM _") |
35 |
35 |
36 parse_translation {* |
|
37 [("\<^fixed>meta_term", fn [t] => Const ("ProtoPure.term", dummyT --> propT) $ t)] |
|
38 *} |
|
39 |
|
40 lemmas [intro?] = termI |
36 lemmas [intro?] = termI |
41 |
37 |
42 |
38 |
43 subsection {* Meta-level conjunction *} |
39 subsection {* Meta-level conjunction *} |
44 |
40 |
45 locale (open) meta_conjunction_syntax = |
41 locale (open) meta_conjunction_syntax = |
46 fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) |
42 fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) |
47 |
|
48 parse_translation {* |
|
49 [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))] |
|
50 *} |
|
51 |
43 |
52 lemma all_conjunction: |
44 lemma all_conjunction: |
53 includes meta_conjunction_syntax |
45 includes meta_conjunction_syntax |
54 shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))" |
46 shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))" |
55 proof |
47 proof |