new attribute [rotated]
authorkleing
Mon Aug 13 04:35:41 2007 +0200 (2007-08-13)
changeset 24238ae70f95e31de
parent 24237 4bf3e084d9b5
child 24239 9f49e5d12a32
new attribute [rotated]
NEWS
src/Pure/Isar/attrib.ML
     1.1 --- a/NEWS	Mon Aug 13 00:23:43 2007 +0200
     1.2 +++ b/NEWS	Mon Aug 13 04:35:41 2007 +0200
     1.3 @@ -292,6 +292,9 @@
     1.4  analogous to the 'rule_format' attribute, but *not* that of the
     1.5  Simplifier (which is usually more generous).
     1.6  
     1.7 +* Isar: the new attribute [rotated n] (default n = 1) rotates the
     1.8 +premises of a theorem by n. Useful in conjunction with drule.
     1.9 +
    1.10  * Isar: the goal restriction operator [N] (default N = 1) evaluates a
    1.11  method expression within a sandbox consisting of the first N
    1.12  sub-goals, which need to exist.  For example, ``simp_all [3]''
     2.1 --- a/src/Pure/Isar/attrib.ML	Mon Aug 13 00:23:43 2007 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Mon Aug 13 04:35:41 2007 +0200
     2.3 @@ -346,6 +346,13 @@
     2.4    syntax (Scan.lift Args.internal_attribute >> Morphism.form) x;
     2.5  
     2.6  
     2.7 +(* attribute rotated *)
     2.8 +
     2.9 +fun rotated_att x = 
    2.10 +  syntax (Scan.lift (Scan.optional Args.int 1) >> 
    2.11 +                    (fn n => Thm.rule_attribute (fn _ => rotate_prems n))) x
    2.12 +
    2.13 +
    2.14  (* theory setup *)
    2.15  
    2.16  val _ = Context.add_setup
    2.17 @@ -375,6 +382,7 @@
    2.18      ("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"),
    2.19      ("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"),
    2.20      ("rule_format", rule_format_att, "result put into standard rule format"),
    2.21 +    ("rotated", rotated_att, "rotated theorem premises"),
    2.22      ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
    2.23        "declaration of definitional transformations"),
    2.24      ("attribute", internal_att, "internal attribute")]);