changeset 51144 | 0ede9e2266a8 |
parent 51093 | 9d7aa2bb097b |
child 51240 | a7a04b449e8b |
--- a/src/HOL/ex/Reflection_Examples.thy Fri Feb 15 08:31:31 2013 +0100 +++ b/src/HOL/ex/Reflection_Examples.thy Fri Feb 15 08:31:31 2013 +0100 @@ -129,7 +129,6 @@ text {* Now we specify on which subterm it should be applied *} lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D" apply (reflection Ifm.simps only: "B \<or> C \<and> (B \<longrightarrow> A \<or> D)") - apply code_simp oops