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.
fixed RuleCases.make (invert flag);
authorwenzelm
Fri, 18 Aug 2000 18:11:10 +0200
changeset 9653 2937a854e3d7
parent 9652 ea1f02d6d65b
child 9654 9754ba005b64
fixed RuleCases.make (invert flag);
src/Pure/Isar/method.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/method.ML	Fri Aug 18 18:06:10 2000 +0200
+++ b/src/Pure/Isar/method.ML	Fri Aug 18 18:11:10 2000 +0200
@@ -296,7 +296,7 @@
 val resolveq_tac = gen_resolveq_tac Tactic.rtac;
 
 fun resolveq_cases_tac open_parms = gen_resolveq_tac (fn (rule, cases) => fn i => fn st =>
-  Seq.map (rpair (RuleCases.make open_parms rule cases)) (Tactic.rtac rule i st));
+  Seq.map (rpair (RuleCases.make (not open_parms) rule cases)) (Tactic.rtac rule i st));
 
 
 (* simple rule *)
isabelle