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.
empty rule_context for multiple goals;
authorwenzelm
Mon, 12 Nov 2001 23:28:49 +0100
changeset 12167 74f92a43bac3
parent 12166 5fc22b8c03e9
child 12168 dc93c2e82205
empty rule_context for multiple goals;
src/Pure/Isar/proof.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/proof.ML	Mon Nov 12 23:28:15 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Nov 12 23:28:49 2001 +0100
@@ -342,7 +342,7 @@
       | subgoals n = ", " ^ string_of_int n ^ " subgoals";
 
     fun prt_names names =
-      (case filter_out (equal "") names of [] => "" | nms => space_implode " and " nms);
+      (case filter_out (equal "") names of [] => "" | nms => " " ^ space_implode " and " nms);
 
     fun prt_goal (_, (i, (((kind, names, _), (goal_facts, thm)), _))) =
       pretty_facts "using " ctxt
@@ -632,7 +632,9 @@
     state'
     |> map_context (autofix props)
     |> put_goal (Some (((kind, names, propss), ([], goal)), after_qed o map_context gen_binds))
-    |> map_context (ProofContext.add_cases (RuleCases.make true goal [rule_contextN]))
+    |> map_context (ProofContext.add_cases
+     (if length props = 1 then RuleCases.make true goal [rule_contextN]
+      else [(rule_contextN, RuleCases.empty)]))
     |> auto_bind_goal props
     |> (if is_chain state then use_facts else reset_facts)
     |> new_block
isabelle