src/FOL/simpdata.ML
changeset 17002 fb9261990ffe
parent 16019 0e1405402d53
child 17325 d9d50222808e
     1.1 --- a/src/FOL/simpdata.ML	Tue Aug 02 19:47:11 2005 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Tue Aug 02 19:47:12 2005 +0200
     1.3 @@ -267,11 +267,11 @@
     1.4  end;
     1.5  
     1.6  val defEX_regroup =
     1.7 -  Simplifier.simproc (Theory.sign_of (the_context ()))
     1.8 +  Simplifier.simproc (the_context ())
     1.9      "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
    1.10  
    1.11  val defALL_regroup =
    1.12 -  Simplifier.simproc (Theory.sign_of (the_context ()))
    1.13 +  Simplifier.simproc (the_context ())
    1.14      "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
    1.15  
    1.16  
    1.17 @@ -337,6 +337,10 @@
    1.18    setmksimps (mksimps mksimps_pairs)
    1.19    setmkcong mk_meta_cong;
    1.20  
    1.21 +fun unfold_tac ss ths =
    1.22 +  ALLGOALS (full_simp_tac
    1.23 +    (Simplifier.inherit_bounds ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
    1.24 +
    1.25  
    1.26  (*intuitionistic simprules only*)
    1.27  val IFOL_ss = FOL_basic_ss