# HG changeset patch
# User wenzelm
# Date 1305382973 -7200
# Node ID a6dafa3d7adaaf2b98cb6bbe36975de1aed4eb0c
# Parent  125bddad6bd656feb10f296f49a9d5a044d934a0
discontinued old / unused addss' (cf. 57f364d1d3b2);

diff -r 125bddad6bd6 -r a6dafa3d7ada src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat May 14 16:12:42 2011 +0200
+++ b/src/Provers/clasimp.ML	Sat May 14 16:22:53 2011 +0200
@@ -19,7 +19,6 @@
 sig
   val addSss: Proof.context -> Proof.context
   val addss: Proof.context -> Proof.context
-  val addss': Proof.context -> Proof.context
   val clarsimp_tac: Proof.context -> int -> tactic
   val mk_auto_tac: Proof.context -> int -> int -> tactic
   val auto_tac: Proof.context -> tactic
@@ -55,8 +54,6 @@
 (*Caution: only one simpset added can be added by each of addSss and addss*)
 val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac;
 val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
-(* FIXME "asm_lr_simp_tac" !? *)
-val addss' = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_lr_simp_tac;
 
 
 (* iffs: addition of rules to simpsets and clasets simultaneously *)