# HG changeset patch
# User wenzelm
# Date 952534358 -3600
# Node ID bdc3ee0d8cb613e72698a4719f77de8f43a454a6
# Parent  2d77b5a723f12c50d8a04ec42f2326d79ee40d90
added 'case_names' and 'params';

diff -r 2d77b5a723f1 -r bdc3ee0d8cb6 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Mar 08 17:51:29 2000 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Mar 08 17:52:38 2000 +0100
@@ -271,6 +271,12 @@
 val local_fold = syntax (local_thmss >> gen_rewrite Tactic.fold_rule);
 
 
+(* rule cases *)
+
+fun case_names x = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names) x;
+fun params x = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params) x;
+
+
 (* misc rules *)
 
 fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
@@ -297,6 +303,8 @@
   ("fold", (global_fold, local_fold), "fold definitions"),
   ("standard", (standard, standard), "put theorem into standard form"),
   ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"),
+  ("case_names", (case_names, case_names), "name rule cases"),
+  ("params", (params, params), "name rule parameters"),
   ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory"),
   ("export", (global_export, local_export), "export theorem from context")];