src/Provers/clasimp.ML
changeset 7132 5c31d06ead04
parent 5985 9481d0cfb86e
child 7153 820c8c8573d9
equal deleted inserted replaced
7131:0b2fe9ec709c 7132:5c31d06ead04
   152 fun get_local_clasimpset ctxt = (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
   152 fun get_local_clasimpset ctxt = (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
   153 
   153 
   154 val clasimp_modifiers = Classical.cla_modifiers @ Simplifier.simp_modifiers;
   154 val clasimp_modifiers = Classical.cla_modifiers @ Simplifier.simp_modifiers;
   155 val clasimp_args = Method.only_sectioned_args clasimp_modifiers;
   155 val clasimp_args = Method.only_sectioned_args clasimp_modifiers;
   156 
   156 
   157 fun clasimp_meth tac ctxt = Method.METHOD0 (tac (get_local_clasimpset ctxt));
   157 fun clasimp_meth tac ctxt = Method.METHOD (fn facts =>
   158 fun clasimp_meth' tac ctxt = Method.METHOD0 (FIRSTGOAL (tac (get_local_clasimpset ctxt)));
   158   ALLGOALS (Method.same_tac facts) THEN tac (get_local_clasimpset ctxt));
       
   159 
       
   160 fun clasimp_meth' tac ctxt = Method.METHOD (fn facts =>
       
   161   FIRSTGOAL (Method.same_tac facts THEN' tac (get_local_clasimpset ctxt)));
   159 
   162 
   160 val clasimp_method = clasimp_args o clasimp_meth;
   163 val clasimp_method = clasimp_args o clasimp_meth;
   161 val clasimp_method' = clasimp_args o clasimp_meth';
   164 val clasimp_method' = clasimp_args o clasimp_meth';
   162 
   165 
   163 
   166