--- 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$.