src/Provers/clasimp.ML
changeset 50107 289181e3e524
parent 47967 c422128d3889
child 50111 9e04e6edc5e7
equal deleted inserted replaced
50106:e12e4ad93183 50107:289181e3e524
    42 structure Blast = Data.Blast;
    42 structure Blast = Data.Blast;
    43 
    43 
    44 
    44 
    45 (* simp as classical wrapper *)
    45 (* simp as classical wrapper *)
    46 
    46 
    47 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
       
    48 val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true);
       
    49 
       
    50 fun clasimp f name tac ctxt =
    47 fun clasimp f name tac ctxt =
    51   Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
    48   Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
    52 
    49 
    53 (*Add a simpset to the claset!*)
    50 (*Add a simpset to the claset!*)
    54 (*Caution: only one simpset added can be added by each of addSss and addss*)
    51 (*Caution: only one simpset added can be added by each of addSss and addss*)