# HG changeset patch
# User berghofe
# Date 1033396325 -7200
# Node ID 57f364d1d3b2304acb2f398980b3d7731d89d462
# Parent  4cecd1e0f4a98801e6b28e299eb0a6283b05d392
Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.

diff -r 4cecd1e0f4a9 -r 57f364d1d3b2 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Mon Sep 30 16:27:38 2002 +0200
+++ b/src/Provers/clasimp.ML	Mon Sep 30 16:32:05 2002 +0200
@@ -8,7 +8,7 @@
 *)
 
 infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2
-  addSss addss addIffs delIffs;
+  addSss addss addss' addIffs delIffs;
 
 signature CLASIMP_DATA =
 sig
@@ -40,6 +40,7 @@
   val delsimps2: clasimpset * thm list -> clasimpset
   val addSss: claset * simpset -> claset
   val addss: claset * simpset -> claset
+  val addss': claset * simpset -> claset
   val addIffs: clasimpset * thm list -> clasimpset
   val delIffs: clasimpset * thm list -> clasimpset
   val AddIffs: thm list -> unit
@@ -110,6 +111,8 @@
                             CHANGED o safe_asm_full_simp_tac ss));
 fun cs addss  ss = Classical.addbefore  (cs, ("asm_full_simp_tac",
                             CHANGED o Simplifier.asm_full_simp_tac ss));
+fun cs addss' ss = Classical.addbefore  (cs, ("asm_full_simp_tac",
+                            CHANGED o Simplifier.asm_lr_simp_tac ss));
 
 
 (* iffs: addition of rules to simpsets and clasets simultaneously *)