doc-src/IsarRef/Thy/Generic.thy
changeset 28754 6f2e67a3dfaa
parent 27248 3c17b824650b
child 28760 cbc435f7b16b
equal deleted inserted replaced
28753:b5926a48c943 28754:6f2e67a3dfaa
    98   the plain @{method rule} method, with forward chaining of current
    98   the plain @{method rule} method, with forward chaining of current
    99   facts.
    99   facts.
   100 
   100 
   101   \item [@{method succeed}] yields a single (unchanged) result; it is
   101   \item [@{method succeed}] yields a single (unchanged) result; it is
   102   the identity of the ``@{text ","}'' method combinator (cf.\
   102   the identity of the ``@{text ","}'' method combinator (cf.\
   103   \secref{sec:syn-meth}).
   103   \secref{sec:proof-meth}).
   104 
   104 
   105   \item [@{method fail}] yields an empty result sequence; it is the
   105   \item [@{method fail}] yields an empty result sequence; it is the
   106   identity of the ``@{text "|"}'' method combinator (cf.\
   106   identity of the ``@{text "|"}'' method combinator (cf.\
   107   \secref{sec:syn-meth}).
   107   \secref{sec:proof-meth}).
   108 
   108 
   109   \end{descr}
   109   \end{descr}
   110 
   110 
   111   \begin{matharray}{rcl}
   111   \begin{matharray}{rcl}
   112     @{attribute_def tagged} & : & \isaratt \\
   112     @{attribute_def tagged} & : & \isaratt \\