Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper context;
authorwenzelm
Fri, 24 Jul 2015 22:20:22 +0200
changeset 60776 2164e7b47454
parent 60775 4592a9118d0b
child 60777 ee811a49c8f6
proper context;
src/Pure/tactic.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/tactic.ML	Fri Jul 24 22:19:36 2015 +0200
+++ b/src/Pure/tactic.ML	Fri Jul 24 22:20:22 2015 +0200
@@ -129,7 +129,7 @@
 fun eresolve_tac ctxt rules = biresolve_tac ctxt (map (pair true) rules);
 
 (*Forward reasoning using destruction rules.*)
-fun forward_tac ctxt rls = resolve_tac ctxt (map make_elim rls) THEN' atac;
+fun forward_tac ctxt rls = resolve_tac ctxt (map make_elim rls) THEN' assume_tac ctxt;
 
 (*Like forward_tac, but deletes the assumption after use.*)
 fun dresolve0_tac rls = eresolve0_tac (map make_elim rls);
isabelle