
diff -r 09253f667beb -r 14a71104a498 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Thu Sep 07 20:59:37 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Thu Sep 07 21:06:55 2000 +0200
@@ -305,43 +305,41 @@
 
 
 \indexisaratt{standard}
-\indexisaratt{elimify}
+\indexisaratt{elimified}
 \indexisaratt{no-vars}
 
 \indexisaratt{THEN}\indexisaratt{COMP}
-\indexisaratt{where}
-\indexisaratt{tag}\indexisaratt{untag}
-\indexisaratt{export}
-\indexisaratt{unfold}\indexisaratt{fold}
+\indexisaratt{where}\indexisaratt{tagged}\indexisaratt{untagged}
+\indexisaratt{unfolded}\indexisaratt{folded}\indexisaratt{exported}
 \begin{matharray}{rcl}
-  tag & : & \isaratt \\
-  untag & : & \isaratt \\[0.5ex]
+  tagged & : & \isaratt \\
+  untagged & : & \isaratt \\[0.5ex]
   THEN & : & \isaratt \\
   COMP & : & \isaratt \\[0.5ex]
   where & : & \isaratt \\[0.5ex]
-  unfold & : & \isaratt \\
-  fold & : & \isaratt \\[0.5ex]
+  unfolded & : & \isaratt \\
+  folded & : & \isaratt \\[0.5ex]
   standard & : & \isaratt \\
-  elimify & : & \isaratt \\
+  elimified & : & \isaratt \\
   no_vars & : & \isaratt \\
-  export^* & : & \isaratt \\
+  exported^* & : & \isaratt \\
 \end{matharray}
 
 \begin{rail}
-  'tag' (nameref+)
+  'tagged' (nameref+)
   ;
-  'untag' name
+  'untagged' name
   ;
   ('THEN' | 'COMP') nat? thmref
   ;
   'where' (name '=' term * 'and')
   ;
-  ('unfold' | 'fold') thmrefs
+  ('unfolded' | 'folded') thmrefs
   ;
 \end{rail}
 
 \begin{descr}
-\item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some
+\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
   theorem.  Tags may be any list of strings that serve as comment for some
   tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
   result).  The first string is considered the tag name, the rest its
@@ -354,24 +352,18 @@
   variables occurring in a theorem.  Unlike instantiation tactics such as
   $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
   have to be specified (e.g.\ $\Var{x@3}$).
-
-\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
-  meta-level definitions throughout a rule.
-
+\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
+  given meta-level definitions throughout a rule.
 \item [$standard$] puts a theorem into the standard form of object-rules, just
   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
-
-\item [$elimify$] turns an destruction rule into an elimination, just as the
+\item [$elimified$] turns an destruction rule into an elimination, just as the
   ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
-
 \item [$no_vars$] replaces schematic variables by free ones; this is mainly
   for tuning output of pretty printed theorems.
-
-\item [$export$] lifts a local result out of the current proof context,
+\item [$exported$] lifts a local result out of the current proof context,
   generalizing all fixed variables and discharging all assumptions.  Note that
   proper incremental export is already done as part of the basic Isar
   machinery.  This attribute is mainly for experimentation.
-
 \end{descr}
 
 
@@ -601,21 +593,30 @@
 
 \subsection{Forward simplification}
 
-\indexisaratt{simplify}\indexisaratt{asm-simplify}
-\indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
+\indexisaratt{simplified}
 \begin{matharray}{rcl}
-  simplify & : & \isaratt \\
-  asm_simplify & : & \isaratt \\
-  full_simplify & : & \isaratt \\
-  asm_full_simplify & : & \isaratt \\
+  simplified & : & \isaratt \\
 \end{matharray}
 
-These attributes provide forward rules for simplification, which should be
-used only very rarely.  There are no separate options for declaring
-simplification rules locally.
+\begin{rail}
+  'simplified' opt?
+  ;
+
+  opt: '(' (noasm | noasmsimp | noasmuse) ')'
+  ;
+\end{rail}
 
-See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more
-information.
+\begin{descr}
+\item [$simplified$] causes a theorem to be simplified according to the
+  current Simplifier context (there are no separate arguments for declaring
+  additional rules).  By default the result is fully simplified, including
+  assumptions and conclusion.  The options $no_asm$ etc.\ restrict the
+  Simplifier in the same way as the for the $simp$ method (see
+  \S\ref{sec:simp}).
+  
+  The $simplified$ operation should be used only very rarely, usually for
+  experimentation only.
+\end{descr}
 
 
 \section{Basic equational reasoning}\label{sec:basic-eq}
@@ -818,7 +819,7 @@
 
 \item [$delrule$] deletes introduction or elimination rules from the context.
   Note that destruction rules would have to be turned into elimination rules
-  first, e.g.\ by using the $elimify$ attribute.
+  first, e.g.\ by using the $elimified$ attribute.
 \end{descr}
 
 




