src/Provers/clasimp.ML
changeset 51703 f2e92fc0c8aa
parent 50111 9e04e6edc5e7
child 51717 9e7d1c139569
equal deleted inserted replaced
51702:dcfab8e87621 51703:f2e92fc0c8aa
    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 fun clasimp f name tac ctxt =
    47 fun clasimp f name tac ctxt = f (ctxt, (name, CHANGED o tac (simpset_of ctxt)));
    48   Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
       
    49 
    48 
    50 (*Add a simpset to the claset!*)
    49 (*Add a simpset to the claset!*)
    51 (*Caution: only one simpset added can be added by each of addSss and addss*)
    50 (*Caution: only one simpset added can be added by each of addSss and addss*)
    52 val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
    51 val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
    53 val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
    52 val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;