equal
deleted
inserted
replaced
55 by blast |
55 by blast |
56 |
56 |
57 lemma tfl_exE: "\<exists>x. P x \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q \<Longrightarrow> Q" |
57 lemma tfl_exE: "\<exists>x. P x \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q \<Longrightarrow> Q" |
58 by blast |
58 by blast |
59 |
59 |
60 ML_file "old_recdef.ML" |
60 ML_file \<open>old_recdef.ML\<close> |
61 |
61 |
62 |
62 |
63 subsection \<open>Rule setup\<close> |
63 subsection \<open>Rule setup\<close> |
64 |
64 |
65 lemmas [recdef_simp] = |
65 lemmas [recdef_simp] = |