# HG changeset patch
# User wenzelm
# Date 898781610 -7200
# Node ID e03460289797bbc8624618b2bc23910274a1f2c4
# Parent  7274f7d101ee5f04a2df3694fb655eaef4352340
added XX_YY_rewrite: simpset -> cterm -> thm;

diff -r 7274f7d101ee -r e03460289797 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Jun 25 15:32:41 1998 +0200
+++ b/src/Provers/simplifier.ML	Thu Jun 25 15:33:30 1998 +0200
@@ -78,6 +78,10 @@
 signature SIMPLIFIER =
 sig
   include BASIC_SIMPLIFIER
+  val          rewrite: simpset -> cterm -> thm
+  val      asm_rewrite: simpset -> cterm -> thm
+  val     full_rewrite: simpset -> cterm -> thm
+  val asm_full_rewrite: simpset -> cterm -> thm
   val setup: (theory -> theory) list
   val get_local_simpset: local_theory -> simpset
   val put_local_simpset: simpset -> local_theory -> local_theory
@@ -404,20 +408,26 @@
 
 
 
-(** simplification meta rules **)
+(** simplification rules and conversions **)
 
-fun simp mode (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) thm =
+fun simp rew mode (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) thm =
   let
     val tacf = solve_all_tac (subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
     fun prover m th = apsome fst (Seq.pull (tacf m th));
-  in
-    Drule.rewrite_thm mode prover mss thm
-  end;
+  in rew mode prover mss thm end;
+
+val simp_thm = simp Drule.rewrite_thm;
+val simp_cterm = simp Drule.rewrite_cterm;
 
-val          simplify = simp (false, false, false);
-val      asm_simplify = simp (false, true, false);
-val     full_simplify = simp (true, false, false);
-val asm_full_simplify = simp (true, true, false);
+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          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);