1.1 --- a/src/Provers/clasimp.ML	Wed Dec 05 03:10:06 2001 +0100
     1.2 +++ b/src/Provers/clasimp.ML	Wed Dec 05 03:11:05 2001 +0100
     1.3 @@ -1,6 +1,7 @@
     1.4  (*  Title:      Provers/clasimp.ML
     1.5      ID:         $Id$
     1.6      Author:     David von Oheimb, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8  
     1.9  Combination of classical reasoner and simplifier (depends on
    1.10  simplifier.ML, splitter.ML classical.ML, blast.ML).
    1.11 @@ -128,13 +129,13 @@
    1.12       simp (ss, [th]))
    1.13    end;
    1.14  
    1.15 -fun delIff ((cs, ss), th) =
    1.16 +fun delIff delcs delss ((cs, ss), th) =
    1.17    let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
    1.18 -    (Classical.delrules (cs, [zero_rotate (th RS Data.iffD2),
    1.19 +    (delcs (cs, [zero_rotate (th RS Data.iffD2),
    1.20          Data.cla_make_elim (zero_rotate (th RS Data.iffD1))])
    1.21 -      handle THM _ => (Classical.delrules (cs, [zero_rotate (th RS Data.notE)])
    1.22 -        handle THM _ => Classical.delrules (cs, [th])),
    1.23 -     Simplifier.delsimps (ss, [th]))
    1.24 +      handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)])
    1.25 +        handle THM _ => delcs (cs, [th])),
    1.26 +     delss (ss, [th]))
    1.27    end;
    1.28  
    1.29  fun store_clasimp (cs, ss) =
    1.30 @@ -144,14 +145,25 @@
    1.31  
    1.32  val op addIffs =
    1.33    foldl (addIff Classical.addSDs Classical.addSEs Classical.addSIs Simplifier.addsimps);
    1.34 -val addIffs' =
    1.35 -  foldl (addIff Classical.addXDs Classical.addXEs Classical.addXIs
    1.36 -    ((fn (ss, _) => ss): Simplifier.simpset * thm list -> Simplifier.simpset));
    1.37 -val op delIffs = foldl delIff;
    1.38 +val op delIffs = foldl (delIff Classical.delrules Simplifier.delsimps);
    1.39  
    1.40  fun AddIffs thms = store_clasimp (clasimpset () addIffs thms);
    1.41  fun DelIffs thms = store_clasimp (clasimpset () delIffs thms);
    1.42  
    1.43 +fun addIffs_global (thy, ths) =
    1.44 +  foldl (addIff ContextRules.addXDs_global ContextRules.addXEs_global
    1.45 +    ContextRules.addXIs_global #1) ((thy, ()), ths) |> #1;
    1.46 +
    1.47 +fun addIffs_local (ctxt, ths) =
    1.48 +  foldl (addIff ContextRules.addXDs_local ContextRules.addXEs_local
    1.49 +    ContextRules.addXIs_local #1) ((ctxt, ()), ths) |> #1;
    1.50 +
    1.51 +fun delIffs_global (thy, ths) =
    1.52 +  foldl (delIff ContextRules.delrules_global #1) ((thy, ()), ths) |> #1;
    1.53 +
    1.54 +fun delIffs_local (ctxt, ths) =
    1.55 +  foldl (delIff ContextRules.delrules_local #1) ((ctxt, ()), ths) |> #1;
    1.56 +
    1.57  end;
    1.58  
    1.59  
    1.60 @@ -164,8 +176,10 @@
    1.61    Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state;
    1.62  
    1.63  
    1.64 -fun clarsimp_tac (cs, ss) = safe_asm_full_simp_tac ss THEN_ALL_NEW
    1.65 -                            Classical.clarify_tac (cs addSss ss);
    1.66 +fun clarsimp_tac (cs, ss) =
    1.67 +  safe_asm_full_simp_tac ss THEN_ALL_NEW
    1.68 +  Classical.clarify_tac (cs addSss ss);
    1.69 +
    1.70  fun Clarsimp_tac i = clarsimp_tac (clasimpset ()) i;
    1.71  
    1.72  
    1.73 @@ -204,9 +218,7 @@
    1.74      end;
    1.75  
    1.76  fun auto_tac css = mk_auto_tac css 4 2;
    1.77 -
    1.78  fun Auto_tac st = auto_tac (clasimpset ()) st;
    1.79 -
    1.80  fun auto () = by Auto_tac;
    1.81  
    1.82  
    1.83 @@ -256,12 +268,14 @@
    1.84  
    1.85  (* attributes *)
    1.86  
    1.87 +fun change_rules f (x, th) = (f (x, [th]), th);
    1.88 +
    1.89  val iff_add_global = change_global_css (op addIffs);
    1.90 -val iff_add_global' = change_global_css (op addIffs');
    1.91 -val iff_del_global = change_global_css (op delIffs);
    1.92 +val iff_add_global' = change_rules addIffs_global;
    1.93 +val iff_del_global = change_global_css (op delIffs) o change_rules delIffs_global;
    1.94  val iff_add_local = change_local_css (op addIffs);
    1.95 -val iff_add_local' = change_local_css (op addIffs');
    1.96 -val iff_del_local = change_local_css (op delIffs);
    1.97 +val iff_add_local' = change_rules addIffs_local;
    1.98 +val iff_del_local = change_local_css (op delIffs) o change_rules delIffs_local;
    1.99  
   1.100  fun iff_att add add' del = Attrib.syntax (Scan.lift
   1.101   (Args.del >> K del ||