equal
deleted
inserted
replaced
24 "(!!x y. PROP P x y) == (!!y x. PROP P x y)" .. |
24 "(!!x y. PROP P x y) == (!!y x. PROP P x y)" .. |
25 |
25 |
26 |
26 |
27 subsection {* Embedded terms *} |
27 subsection {* Embedded terms *} |
28 |
28 |
29 locale (open) meta_term_syntax = |
29 locale meta_term_syntax = |
30 fixes meta_term :: "'a => prop" ("TERM _") |
30 fixes meta_term :: "'a => prop" ("TERM _") |
31 |
31 |
32 lemmas [intro?] = termI |
32 lemmas [intro?] = termI |
33 |
33 |
34 |
34 |
35 subsection {* Meta-level conjunction *} |
35 subsection {* Meta-level conjunction *} |
36 |
36 |
37 locale (open) meta_conjunction_syntax = |
37 locale meta_conjunction_syntax = |
38 fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) |
38 fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) |
39 |
39 |
40 lemma all_conjunction: |
40 lemma all_conjunction: |
41 includes meta_conjunction_syntax |
41 includes meta_conjunction_syntax |
42 shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))" |
42 shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))" |