equal
deleted
inserted
replaced
15 begin |
15 begin |
16 |
16 |
17 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
17 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
18 by auto |
18 by auto |
19 |
19 |
20 lemma eq_sym_Unity_imp: "x = (() = ()) \<Longrightarrow> x" |
20 lemma eq_sym_Unity_conv: "(x = (() = ())) = x" |
21 by blast |
21 by blast |
22 |
22 |
23 lemma unit_case_Unity: "(case u of () => f) = f" |
23 lemma unit_case_Unity: "(case u of () => f) = f" |
24 by (cases u) (hypsubst, rule unit.cases) |
24 by (cases u) (hypsubst, rule unit.cases) |
25 |
25 |