added asm_lr_simplify/asm_lr_rewrite and adapted asm_full_simplify/asm_full_rewrite to match to corresponding simp_tacs
authorschirmer
Fri May 28 21:09:56 2004 +0200 (2004-05-28)
changeset 14814c6b91c8aee1d
parent 14813 826edbc317e6
child 14815 77a509d83163
added asm_lr_simplify/asm_lr_rewrite and adapted asm_full_simplify/asm_full_rewrite to match to corresponding simp_tacs
src/Provers/simplifier.ML
     1.1 --- a/src/Provers/simplifier.ML	Fri May 28 11:20:04 2004 +0200
     1.2 +++ b/src/Provers/simplifier.ML	Fri May 28 21:09:56 2004 +0200
     1.3 @@ -81,6 +81,7 @@
     1.4    val          simplify: simpset -> thm -> thm
     1.5    val      asm_simplify: simpset -> thm -> thm
     1.6    val     full_simplify: simpset -> thm -> thm
     1.7 +  val   asm_lr_simplify: simpset -> thm -> thm
     1.8    val asm_full_simplify: simpset -> thm -> thm
     1.9  end;
    1.10  
    1.11 @@ -94,6 +95,7 @@
    1.12    val          rewrite: simpset -> cterm -> thm
    1.13    val      asm_rewrite: simpset -> cterm -> thm
    1.14    val     full_rewrite: simpset -> cterm -> thm
    1.15 +  val   asm_lr_rewrite: simpset -> cterm -> thm
    1.16    val asm_full_rewrite: simpset -> cterm -> thm
    1.17    val print_local_simpset: Proof.context -> unit
    1.18    val get_local_simpset: Proof.context -> simpset
    1.19 @@ -454,12 +456,14 @@
    1.20  val          simplify = simp_thm (false, false, false);
    1.21  val      asm_simplify = simp_thm (false, true, false);
    1.22  val     full_simplify = simp_thm (true, false, false);
    1.23 -val asm_full_simplify = simp_thm (true, true, false);
    1.24 +val   asm_lr_simplify = simp_thm (true, true, false);
    1.25 +val asm_full_simplify = simp_thm (true, true, true);
    1.26  
    1.27  val          rewrite = simp_cterm (false, false, false);
    1.28  val      asm_rewrite = simp_cterm (false, true, false);
    1.29  val     full_rewrite = simp_cterm (true, false, false);
    1.30 -val asm_full_rewrite = simp_cterm (true, true, false);
    1.31 +val   asm_lr_rewrite = simp_cterm (true, true, false);
    1.32 +val asm_full_rewrite = simp_cterm (true, true, true);
    1.33  
    1.34  
    1.35