src/Provers/clasimp.ML

 
 signature CLASIMP =
 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
   val force_tac: Proof.context -> int -> tactic
   val fast_simp_tac: Proof.context -> int -> tactic

 
 (*Add a simpset to the claset!*)
 (*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 *)
 
 local