# HG changeset patch # User wenzelm # Date 1138620005 -3600 # Node ID 99124f3beccfb3922733b0d5a47ad82c2204a7b0 # Parent afe45058241aabe6c0a0ad5720ad6ce03b09caae 'fixes': support plain vars; classical attributes: optional weight -- ignored by automated tools; diff -r afe45058241a -r 99124f3beccf doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Mon Jan 30 10:13:28 2006 +0100 +++ b/doc-src/IsarRef/generic.tex Mon Jan 30 12:20:05 2006 +0100 @@ -124,7 +124,7 @@ ; contextelem: fixes | constrains | assumes | defines | notes | includes ; - fixes: 'fixes' (name ('::' type)? structmixfix? + 'and') + fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and') ; constrains: 'constrains' (name '::' type + 'and') ; @@ -1145,7 +1145,7 @@ \end{matharray} \begin{rail} - ('intro' | 'elim' | 'dest') ('!' | () | '?') + ('intro' | 'elim' | 'dest') ('!' | () | '?') nat? ; 'rule' 'del' ; @@ -1158,13 +1158,15 @@ \item [$\isarcmd{print_claset}$] prints the collection of rules declared to the Classical Reasoner, which is also known as ``simpset'' internally \cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply. - + \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and destruction rules, respectively. By default, rules are considered as \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a single ``!'' classifies as \emph{safe}. Rule declarations marked by ``?'' - coincide with those of Isabelle/Pure, cf.\ \S\ref{sec:pure-meth-att} (i.e.\ - are only applied in single steps of the $rule$ method). + coincide with those of Isabelle/Pure, cf.\ \S\ref{sec:pure-meth-att} (i.e.\ + are only applied in single steps of the $rule$ method). The optional + natural number specifies an explicit weight argument, which is ignored by + automated tools, but determines the search order of single rule steps. \item [$rule~del$] deletes introduction, elimination, or destruction rules from the context.