# HG changeset patch
# User schirmer
# Date 1085771396 -7200
# Node ID c6b91c8aee1db54423cbdd7eb7e1353caaa3bec4
# Parent  826edbc317e66821d37b45b85b051c309867b097
added asm_lr_simplify/asm_lr_rewrite and adapted asm_full_simplify/asm_full_rewrite to match to corresponding simp_tacs

diff -r 826edbc317e6 -r c6b91c8aee1d src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri May 28 11:20:04 2004 +0200
+++ b/src/Provers/simplifier.ML	Fri May 28 21:09:56 2004 +0200
@@ -81,6 +81,7 @@
   val          simplify: simpset -> thm -> thm
   val      asm_simplify: simpset -> thm -> thm
   val     full_simplify: simpset -> thm -> thm
+  val   asm_lr_simplify: simpset -> thm -> thm
   val asm_full_simplify: simpset -> thm -> thm
 end;
 
@@ -94,6 +95,7 @@
   val          rewrite: simpset -> cterm -> thm
   val      asm_rewrite: simpset -> cterm -> thm
   val     full_rewrite: simpset -> cterm -> thm
+  val   asm_lr_rewrite: simpset -> cterm -> thm
   val asm_full_rewrite: simpset -> cterm -> thm
   val print_local_simpset: Proof.context -> unit
   val get_local_simpset: Proof.context -> simpset
@@ -454,12 +456,14 @@
 val          simplify = simp_thm (false, false, false);
 val      asm_simplify = simp_thm (false, true, false);
 val     full_simplify = simp_thm (true, false, false);
-val asm_full_simplify = simp_thm (true, true, false);
+val   asm_lr_simplify = simp_thm (true, true, false);
+val asm_full_simplify = simp_thm (true, true, true);
 
 val          rewrite = simp_cterm (false, false, false);
 val      asm_rewrite = simp_cterm (false, true, false);
 val     full_rewrite = simp_cterm (true, false, false);
-val asm_full_rewrite = simp_cterm (true, true, false);
+val   asm_lr_rewrite = simp_cterm (true, true, false);
+val asm_full_rewrite = simp_cterm (true, true, true);