src/Provers/clasimp.ML
changeset 42805 a6dafa3d7ada
parent 42793 88bee9f6eec7
child 43331 01f051619eee
--- 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 *)