src/Provers/rulify.ML
changeset 9941 fe05af7ec816
parent 9884 8cc344b3435e
     1.1 --- a/src/Provers/rulify.ML	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/Provers/rulify.ML	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -19,8 +19,8 @@
     1.4  signature RULIFY =
     1.5  sig
     1.6    include BASIC_RULIFY
     1.7 -  val rulified: 'a attribute
     1.8 -  val rulified_no_asm: 'a attribute
     1.9 +  val rule_format: 'a attribute
    1.10 +  val rule_format_no_asm: 'a attribute
    1.11    val setup: (theory -> theory) list
    1.12  end;
    1.13  
    1.14 @@ -38,11 +38,11 @@
    1.15  
    1.16  (* attributes *)
    1.17  
    1.18 -fun rulified x = Drule.rule_attribute (fn _ => rulify) x;
    1.19 -fun rulified_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
    1.20 +fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
    1.21 +fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
    1.22  
    1.23 -fun rulified_att x = Attrib.syntax
    1.24 -  (Scan.lift (Args.parens (Args.$$$ "no_asm") >> K rulified_no_asm || Scan.succeed rulified)) x;
    1.25 +fun rule_format_att x = Attrib.syntax
    1.26 +  (Scan.lift (Args.parens (Args.$$$ "no_asm") >> K rule_format_no_asm || Scan.succeed rule_format)) x;
    1.27  
    1.28  
    1.29  (* qed commands *)
    1.30 @@ -60,6 +60,6 @@
    1.31  
    1.32  val setup =
    1.33   [Attrib.add_attributes
    1.34 -  [("rulified", (rulified_att, rulified_att), "result put into standard rule form")]];
    1.35 +  [("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")]];
    1.36  
    1.37  end;