Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/clasimp.ML
changeset 8168 9d2ac5439089
parent 8154 dab09e1ad594
child 8469 482c301041b4
equal deleted inserted replaced
8167:7574835ed01e 8168:9d2ac5439089 
   156 
   156 
   157 fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
 
   157 fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
 
   158   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
 
   158   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
 
   159 
   159 
   160 fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
 
   160 fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
 
   161   FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
 
   161   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
 
   162 
   162 
   163 val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
 
   163 val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
 
   164 val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
 
   164 val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
 
   165 
   165 
   166 
   166
isabelle