src/Pure/Isar/attrib.ML
changeset 18236 dd445f5cb28e
parent 18037 1095d2213b9d
child 18243 1287b15f27ef
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Nov 23 18:52:02 2005 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Nov 23 18:52:03 2005 +0100
     1.3 @@ -439,6 +439,8 @@
     1.4  
     1.5  fun consumes x = syntax (Scan.lift (Scan.optional Args.nat 1) >> RuleCases.consumes) x;
     1.6  fun case_names x = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names) x;
     1.7 +fun case_conclusion x =
     1.8 +  syntax (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion) x;
     1.9  fun params x = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params) x;
    1.10  
    1.11  
    1.12 @@ -519,6 +521,7 @@
    1.13    ("eta_long", (eta_long, eta_long), "put theorem into eta long beta normal form"),
    1.14    ("consumes", (consumes, consumes), "number of consumed facts"),
    1.15    ("case_names", (case_names, case_names), "named rule cases"),
    1.16 +  ("case_clusion", (case_conclusion, case_conclusion), "named conclusion of rule cases"),
    1.17    ("params", (params, params), "named rule parameters"),
    1.18    ("atomize", (no_args ObjectLogic.declare_atomize, no_args undef_local_attribute),
    1.19      "declaration of atomize rule"),