equal
deleted
inserted
replaced
11 theory BNF_FP |
11 theory BNF_FP |
12 imports BNF_Comp BNF_Wrap |
12 imports BNF_Comp BNF_Wrap |
13 keywords |
13 keywords |
14 "defaults" |
14 "defaults" |
15 begin |
15 begin |
|
16 |
|
17 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
|
18 by auto |
16 |
19 |
17 lemma eq_sym_Unity_imp: "x = (() = ()) \<Longrightarrow> x" |
20 lemma eq_sym_Unity_imp: "x = (() = ()) \<Longrightarrow> x" |
18 by blast |
21 by blast |
19 |
22 |
20 lemma unit_case_Unity: "(case u of () => f) = f" |
23 lemma unit_case_Unity: "(case u of () => f) = f" |