# HG changeset patch
# User wenzelm
# Date 1391274303 -3600
# Node ID cb5ef74b32f9a14fc85ba87e7bb34e4191f08831
# Parent  08f2ebb6507891f1ee5ddbbcbe5b2dc4612e255b
proper Simplifier method setup;

diff -r 08f2ebb65078 -r cb5ef74b32f9 src/Sequents/LK.thy
--- a/src/Sequents/LK.thy	Sat Feb 01 18:00:28 2014 +0100
+++ b/src/Sequents/LK.thy	Sat Feb 01 18:05:03 2014 +0100
@@ -202,19 +202,21 @@
 
 ML_file "simpdata.ML"
 setup {* map_theory_simpset (put_simpset LK_ss) *}
+setup {* Simplifier.method_setup [] *}
 
 
 text {* To create substition rules *}
 
 lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
-  apply (tactic {* asm_simp_tac (put_simpset LK_basic_ss @{context}) 1 *})
-  done
+  by simp
 
 lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
   apply (rule_tac P = Q in cut)
-   apply (tactic {* simp_tac (@{context} addsimps @{thms if_P}) 2 *})
+   prefer 2
+   apply (simp add: if_P)
   apply (rule_tac P = "~Q" in cut)
-   apply (tactic {* simp_tac (@{context} addsimps @{thms if_not_P}) 2 *})
+   prefer 2
+   apply (simp add: if_not_P)
   apply fast
   done
 
diff -r 08f2ebb65078 -r cb5ef74b32f9 src/Sequents/LK/Nat.thy
--- a/src/Sequents/LK/Nat.thy	Sat Feb 01 18:00:28 2014 +0100
+++ b/src/Sequents/LK/Nat.thy	Sat Feb 01 18:05:03 2014 +0100
@@ -36,7 +36,7 @@
 
 lemma Suc_n_not_n: "|- Suc(k) ~= k"
   apply (rule_tac n = k in induct)
-  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms Suc_neq_0}) 1 *})
+  apply simp
   apply (fast add!: Suc_inject_rule)
   done
 
@@ -54,26 +54,22 @@
 
 lemma add_assoc: "|- (k+m)+n = k+(m+n)"
   apply (rule_tac n = "k" in induct)
-  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
-  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
+  apply simp_all
   done
 
 lemma add_0_right: "|- m+0 = m"
   apply (rule_tac n = "m" in induct)
-  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
-  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
+  apply simp_all
   done
 
 lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)"
   apply (rule_tac n = "m" in induct)
-  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
-  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
+  apply simp_all
   done
 
 lemma "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)"
   apply (rule_tac n = "i" in induct)
-  apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *})
-  apply (tactic {* asm_simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *})
+  apply simp_all
   done
 
 end