src/Provers/clasimp.ML
changeset 50111 9e04e6edc5e7
parent 50107 289181e3e524
child 51703 f2e92fc0c8aa
equal deleted inserted replaced
50110:c933c635843a 50111:9e04e6edc5e7
    47 fun clasimp f name tac ctxt =
    47 fun clasimp f name tac ctxt =
    48   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;
    49 
    49 
    50 (*Add a simpset to the claset!*)
    50 (*Add a simpset to the claset!*)
    51 (*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*)
    52 val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac;
    52 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;
    53 val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
    54 
    54 
    55 
    55 
    56 (* iffs: addition of rules to simpsets and clasets simultaneously *)
    56 (* iffs: addition of rules to simpsets and clasets simultaneously *)
    57 
    57 
   110 
   110 
   111 
   111 
   112 (* tactics *)
   112 (* tactics *)
   113 
   113 
   114 fun clarsimp_tac ctxt =
   114 fun clarsimp_tac ctxt =
   115   safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW
   115   Simplifier.safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW
   116   Classical.clarify_tac (addSss ctxt);
   116   Classical.clarify_tac (addSss ctxt);
   117 
   117 
   118 
   118 
   119 (* auto_tac *)
   119 (* auto_tac *)
   120 
   120