# HG changeset patch
# User wenzelm
# Date 981148763 -3600
# Node ID 568eb11f8d522832d3d5ae7d85e843ea4181ac08
# Parent  fc3124a54ca970a4b3c28d8d3c92c5e5872e988c
added hol_simplify, hol_rewrite_cterm;

diff -r fc3124a54ca9 -r 568eb11f8d52 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Feb 02 22:19:02 2001 +0100
+++ b/src/HOL/simpdata.ML	Fri Feb 02 22:19:23 2001 +0100
@@ -389,6 +389,11 @@
      addcongs [imp_cong]
      addsplits [split_if];
 
+fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
+fun hol_rewrite_cterm rews =
+  #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews);
+
+
 (*Simplifies x assuming c and y assuming ~c*)
 val prems = Goalw [if_def]
   "[| b=c; c ==> x=u; ~c ==> y=v |] ==> \