# HG changeset patch
# User kleing
# Date 1186972541 -7200
# Node ID ae70f95e31de89cc336b1e6262baa7365107bc01
# Parent  4bf3e084d9b56744dc658fa1becb9672d7cb6b4e
new attribute [rotated]

diff -r 4bf3e084d9b5 -r ae70f95e31de NEWS
--- a/NEWS	Mon Aug 13 00:23:43 2007 +0200
+++ b/NEWS	Mon Aug 13 04:35:41 2007 +0200
@@ -292,6 +292,9 @@
 analogous to the 'rule_format' attribute, but *not* that of the
 Simplifier (which is usually more generous).
 
+* Isar: the new attribute [rotated n] (default n = 1) rotates the
+premises of a theorem by n. Useful in conjunction with drule.
+
 * Isar: the goal restriction operator [N] (default N = 1) evaluates a
 method expression within a sandbox consisting of the first N
 sub-goals, which need to exist.  For example, ``simp_all [3]''
diff -r 4bf3e084d9b5 -r ae70f95e31de src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Aug 13 00:23:43 2007 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Aug 13 04:35:41 2007 +0200
@@ -346,6 +346,13 @@
   syntax (Scan.lift Args.internal_attribute >> Morphism.form) x;
 
 
+(* attribute rotated *)
+
+fun rotated_att x = 
+  syntax (Scan.lift (Scan.optional Args.int 1) >> 
+                    (fn n => Thm.rule_attribute (fn _ => rotate_prems n))) x
+
+
 (* theory setup *)
 
 val _ = Context.add_setup
@@ -375,6 +382,7 @@
     ("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"),
     ("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"),
     ("rule_format", rule_format_att, "result put into standard rule format"),
+    ("rotated", rotated_att, "rotated theorem premises"),
     ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
       "declaration of definitional transformations"),
     ("attribute", internal_att, "internal attribute")]);