# HG changeset patch
# User wenzelm
# Date 1132768323 -3600
# Node ID dd445f5cb28ea9744ed3a87ca366900668355026
# Parent  63da52e2d6dcd72d8839c7f564db9d33b911ba9b
added case_conclusion attribute;

diff -r 63da52e2d6dc -r dd445f5cb28e src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Nov 23 18:52:02 2005 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Nov 23 18:52:03 2005 +0100
@@ -439,6 +439,8 @@
 
 fun consumes x = syntax (Scan.lift (Scan.optional Args.nat 1) >> RuleCases.consumes) x;
 fun case_names x = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names) x;
+fun case_conclusion x =
+  syntax (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion) x;
 fun params x = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params) x;
 
 
@@ -519,6 +521,7 @@
   ("eta_long", (eta_long, eta_long), "put theorem into eta long beta normal form"),
   ("consumes", (consumes, consumes), "number of consumed facts"),
   ("case_names", (case_names, case_names), "named rule cases"),
+  ("case_clusion", (case_conclusion, case_conclusion), "named conclusion of rule cases"),
   ("params", (params, params), "named rule parameters"),
   ("atomize", (no_args ObjectLogic.declare_atomize, no_args undef_local_attribute),
     "declaration of atomize rule"),