# 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 |] ==> \