Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
discontinued old / unused addss' (cf. 57f364d1d3b2);
authorwenzelm
Sat, 14 May 2011 16:22:53 +0200
changeset 42805 a6dafa3d7ada
parent 42804 125bddad6bd6
child 42806 4b660cdab9b7
discontinued old / unused addss' (cf. 57f364d1d3b2);
src/Provers/clasimp.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle