1.1 --- a/src/Provers/clasimp.ML	Fri Mar 31 21:57:14 2000 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Fri Mar 31 21:58:34 2000 +0200
     1.3 @@ -45,6 +45,8 @@
     1.4    val force_tac	  : clasimpset  -> int -> tactic
     1.5    val Force_tac	  : int -> tactic
     1.6    val force	  : int -> unit
     1.7 +  val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
     1.8 +  val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
     1.9    val setup	  : (theory -> theory) list
    1.10  end;
    1.11  
    1.12 @@ -148,6 +150,27 @@
    1.13  fun force i = by (Force_tac i);
    1.14  
    1.15  
    1.16 +(* attributes *)
    1.17 +
    1.18 +fun change_global_css f (thy, th) =
    1.19 +  let
    1.20 +    val cs_ref = Classical.claset_ref_of thy;
    1.21 +    val ss_ref = Simplifier.simpset_ref_of thy;
    1.22 +    val (cs', ss') = f ((! cs_ref, ! ss_ref), [th]);
    1.23 +  in cs_ref := cs'; ss_ref := ss'; (thy, th) end;
    1.24 +
    1.25 +fun change_local_css f (ctxt, th) =
    1.26 +  let
    1.27 +    val cs = Classical.get_local_claset ctxt;
    1.28 +    val ss = Simplifier.get_local_simpset ctxt;
    1.29 +    val (cs', ss') = f ((cs, ss), [th]);
    1.30 +    val ctxt' =
    1.31 +      ctxt
    1.32 +      |> Classical.put_local_claset cs'
    1.33 +      |> Simplifier.put_local_simpset ss';
    1.34 +  in (ctxt', th) end;
    1.35 +
    1.36 +
    1.37  (* methods *)
    1.38  
    1.39  fun get_local_clasimpset ctxt =