# HG changeset patch
# User wenzelm
# Date 1123004833 -7200
# Node ID b902e11b3df1319513c301815903e5925606d678
# Parent  fb9261990ffe734746e0215aec2e284118953e4d
added unfold_tac (Simplifier.inherit_bounds);

diff -r fb9261990ffe -r b902e11b3df1 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Aug 02 19:47:12 2005 +0200
+++ b/src/HOL/simpdata.ML	Tue Aug 02 19:47:13 2005 +0200
@@ -315,6 +315,10 @@
     setmkeqTrue mk_eq_True
     setmkcong mk_meta_cong;
 
+fun unfold_tac ss ths =
+  ALLGOALS (full_simp_tac
+    (Simplifier.inherit_bounds ss (Simplifier.clear_ss HOL_basic_ss) addsimps ths));
+
 (*In general it seems wrong to add distributive laws by default: they
   might cause exponential blow-up.  But imp_disjL has been in for a while
   and cannot be removed without affecting existing proofs.  Moreover,
@@ -444,4 +448,4 @@
             REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
             SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   end;
-end;
\ No newline at end of file
+end;