doc-src/IsarRef/generic.tex

 \begin{matharray}{rcl}
   \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
   \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
   \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
   \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
-  \isarcmd{print_trans_rules} & : & \isarkeep{theory~|~proof} \\
+  \isarcmd{print_trans_rules}^* & : & \isarkeep{theory~|~proof} \\
   trans & : & \isaratt \\
 \end{matharray}
 
 Calculational proof is forward reasoning with implicit application of
 transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains

   \quad \BG \\
   \qquad \FIX{thesis} \\
   \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
   \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
   \quad \EN \\
-  \quad \FIX{\vec x}~\ASSUMENAME^{\ast}~{a}~{\vec\phi} \\
+  \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
 \end{matharray}
 
 Typically, the soundness proof is relatively straight-forward, often just by
 canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
 $\BY{blast}$ (see \S\ref{sec:classical-auto}).  Accordingly, the ``$that$''

 \begin{rail}
   'tagged' (nameref+)
   ;
   'untagged' name
   ;
-  ('THEN' | 'COMP') nat? thmref
+  ('THEN' | 'COMP') ('[' nat ']')? thmref
   ;
   'where' (name '=' term * 'and')
   ;
   ('unfolded' | 'folded') thmrefs
   ;

 \subsection{Declaring rules}
 
 \indexisarcmd{print-simpset}
 \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
 \begin{matharray}{rcl}
-  print_simpset & : & \isarkeep{theory~|~proof} \\
+  print_simpset^* & : & \isarkeep{theory~|~proof} \\
   simp & : & \isaratt \\
   cong & : & \isaratt \\
   split & : & \isaratt \\
 \end{matharray}
 

 
 \indexisarcmd{print-claset}
 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
 \indexisaratt{iff}\indexisaratt{rule}
 \begin{matharray}{rcl}
-  print_claset & : & \isarkeep{theory~|~proof} \\
+  print_claset^* & : & \isarkeep{theory~|~proof} \\
   intro & : & \isaratt \\
   elim & : & \isaratt \\
   dest & : & \isaratt \\
   rule & : & \isaratt \\
   iff & : & \isaratt \\