src/HOL/simpdata.ML
changeset 11034 568eb11f8d52
parent 11003 ee0838d89deb
child 11162 9e2ec5f02217
     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 |] ==> \