# HG changeset patch
# User kleing
# Date 1188083960 -7200
# Node ID 76372c3847a29e9c3e6768c59b01593355a54357
# Parent  fcf429a4e923858aabd0a86829074b682044c2cd
described 'rotated' attribute

diff -r fcf429a4e923 -r 76372c3847a2 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sat Aug 25 09:22:22 2007 +0200
+++ b/doc-src/IsarRef/generic.tex	Sun Aug 26 01:19:20 2007 +0200
@@ -912,6 +912,7 @@
   COMP & : & \isaratt \\[0.5ex]
   unfolded & : & \isaratt \\
   folded & : & \isaratt \\[0.5ex]
+  rotated & : & \isaratt \\
   elim_format & : & \isaratt \\
   standard^* & : & \isaratt \\
   no_vars^* & : & \isaratt \\
@@ -926,6 +927,7 @@
   ;
   ('unfolded' | 'folded') thmrefs
   ;
+  'rotated' ( int )?
 \end{rail}
 
 \begin{descr}
@@ -945,6 +947,8 @@
 \item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back
   again the given definitions throughout a rule.
 
+\item [$rotated~n$] rotate the premises of a theorem by $n$ (default 1).
+
 \item [$elim_format$] turns a destruction rule into elimination rule format,
   by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP
   B$.