# HG changeset patch
# User nipkow
# Date 889552940 -3600
# Node ID d2e44673c21ed53dee206cdc71b94b3eaec16e7e
# Parent  c8a8482a812488451fbd408958de203fd95ef22e
The new asm_lr_simp_tac is the old asm_full_simp_tac.
The new asm_full_simp_tac also does a limited amount of mutual simplification.

diff -r c8a8482a8124 -r d2e44673c21e src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Tue Mar 10 18:33:13 1998 +0100
+++ b/src/Provers/simplifier.ML	Tue Mar 10 19:02:20 1998 +0100
@@ -66,11 +66,13 @@
   val               simp_tac: simpset -> int -> tactic
   val           asm_simp_tac: simpset -> int -> tactic
   val          full_simp_tac: simpset -> int -> tactic
+  val        asm_lr_simp_tac: simpset -> int -> tactic
   val      asm_full_simp_tac: simpset -> int -> tactic
   val safe_asm_full_simp_tac: simpset -> int -> tactic
   val               Simp_tac:            int -> tactic
   val           Asm_simp_tac:            int -> tactic
   val          Full_simp_tac:            int -> tactic
+  val        Asm_lr_simp_tac:            int -> tactic
   val      Asm_full_simp_tac:            int -> tactic
   val          simplify: simpset -> thm -> thm
   val      asm_simplify: simpset -> thm -> thm
@@ -326,7 +328,8 @@
 val          simp_tac = gen_simp_tac (false, false, false);
 val      asm_simp_tac = gen_simp_tac (false, true, false);
 val     full_simp_tac = gen_simp_tac (true,  false, false);
-val asm_full_simp_tac = gen_simp_tac (true,  true, false);
+val   asm_lr_simp_tac = gen_simp_tac (true,  true, false);
+val asm_full_simp_tac = gen_simp_tac (true,  true, true);
 
 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
 val safe_asm_full_simp_tac = basic_gen_simp_tac (true, true, false);
@@ -336,6 +339,7 @@
 fun          Simp_tac i st =          simp_tac (simpset ()) i st;
 fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
 fun     Full_simp_tac i st =     full_simp_tac (simpset ()) i st;
+fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
 fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;