added unfold_tac (Simplifier.inherit_bounds);
authorwenzelm
Tue Aug 02 19:47:13 2005 +0200 (2005-08-02)
changeset 17003b902e11b3df1
parent 17002 fb9261990ffe
child 17004 6a0d8ecf65f1
added unfold_tac (Simplifier.inherit_bounds);
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Tue Aug 02 19:47:12 2005 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Tue Aug 02 19:47:13 2005 +0200
     1.3 @@ -315,6 +315,10 @@
     1.4      setmkeqTrue mk_eq_True
     1.5      setmkcong mk_meta_cong;
     1.6  
     1.7 +fun unfold_tac ss ths =
     1.8 +  ALLGOALS (full_simp_tac
     1.9 +    (Simplifier.inherit_bounds ss (Simplifier.clear_ss HOL_basic_ss) addsimps ths));
    1.10 +
    1.11  (*In general it seems wrong to add distributive laws by default: they
    1.12    might cause exponential blow-up.  But imp_disjL has been in for a while
    1.13    and cannot be removed without affecting existing proofs.  Moreover,
    1.14 @@ -444,4 +448,4 @@
    1.15              REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
    1.16              SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
    1.17    end;
    1.18 -end;
    1.19 \ No newline at end of file
    1.20 +end;