src/Pure/Isar/attrib.ML
changeset 9941 fe05af7ec816
parent 9902 1ea354905d88
child 9952 24914e42b857
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -269,7 +269,7 @@
     1.4  (* misc rules *)
     1.5  
     1.6  fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
     1.7 -fun elimified x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
     1.8 +fun elim_format x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
     1.9  fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x;
    1.10  
    1.11  fun exported_global x = no_args (Drule.rule_attribute (Proof.export_thm o ProofContext.init)) x;
    1.12 @@ -292,7 +292,7 @@
    1.13    ("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"),
    1.14    ("folded", (folded_global, folded_local), "folded definitions"),
    1.15    ("standard", (standard, standard), "result put into standard form"),
    1.16 -  ("elimified", (elimified, elimified), "destruct rule turned into elimination rule"),
    1.17 +  ("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"),
    1.18    ("no_vars", (no_vars, no_vars), "frozen schematic vars"),
    1.19    ("case_names", (case_names, case_names), "named rule cases"),
    1.20    ("params", (params, params), "named rule parameters"),