src/Sequents/LK.thy
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>