added hol_simplify, hol_rewrite_cterm;
authorwenzelm
Fri Feb 02 22:19:23 2001 +0100 (2001-02-02)
changeset 11034568eb11f8d52
parent 11033 fc3124a54ca9
child 11035 bad7568e76e0
added hol_simplify, hol_rewrite_cterm;
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Fri Feb 02 22:19:02 2001 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Fri Feb 02 22:19:23 2001 +0100
     1.3 @@ -389,6 +389,11 @@
     1.4       addcongs [imp_cong]
     1.5       addsplits [split_if];
     1.6  
     1.7 +fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
     1.8 +fun hol_rewrite_cterm rews =
     1.9 +  #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews);
    1.10 +
    1.11 +
    1.12  (*Simplifies x assuming c and y assuming ~c*)
    1.13  val prems = Goalw [if_def]
    1.14    "[| b=c; c ==> x=u; ~c ==> y=v |] ==> \