Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/simplifier.ML
changeset 14814 c6b91c8aee1d
parent 13605 528f7489a403
child 15006 107e4dfd3b96 
--- 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);
isabelle