| changeset 49591 | 91b228e26348 |
| parent 49590 | 43e2d0e10876 |
| child 49636 | b7256a88a84b |
--- a/src/HOL/BNF/BNF_FP.thy Wed Sep 26 10:00:59 2012 +0200 +++ b/src/HOL/BNF/BNF_FP.thy Wed Sep 26 10:00:59 2012 +0200 @@ -17,7 +17,7 @@ lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" by auto -lemma eq_sym_Unity_imp: "x = (() = ()) \<Longrightarrow> x" +lemma eq_sym_Unity_conv: "(x = (() = ())) = x" by blast lemma unit_case_Unity: "(case u of () => f) = f"