# HG changeset patch
# User wenzelm
# Date 1469039061 -7200
# Node ID 045490f55f691915171252faa07e76c590d77663
# Parent  58980a8b2faff857c5d6feb4885b2549c8c853ac
tuned;

diff -r 58980a8b2faf -r 045490f55f69 src/Sequents/LK.thy
--- a/src/Sequents/LK.thy	Wed Jul 20 16:18:10 2016 +0200
+++ b/src/Sequents/LK.thy	Wed Jul 20 20:24:21 2016 +0200
@@ -205,7 +205,7 @@
 setup \<open>Simplifier.method_setup []\<close>
 
 
-text \<open>To create substition rules\<close>
+text \<open>To create substitution rules\<close>
 
 lemma eq_imp_subst: "\<turnstile> a = b \<Longrightarrow> $H, A(a), $G \<turnstile> $E, A(b), $F"
   by simp