changeset 69605 | a96320074298 |
parent 69593 | 3dda49e08b9d |
--- a/src/Sequents/LK.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/Sequents/LK.thy Sun Jan 06 15:04:34 2019 +0100 @@ -200,7 +200,7 @@ lemma eq_sym_conv: "\<turnstile> x = y \<longleftrightarrow> y = x" by (fast add!: subst) -ML_file "simpdata.ML" +ML_file \<open>simpdata.ML\<close> setup \<open>map_theory_simpset (put_simpset LK_ss)\<close> setup \<open>Simplifier.method_setup []\<close>