1.1 --- a/doc-src/IsarRef/Thy/pure.thy	Fri May 02 22:48:51 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/pure.thy	Fri May 02 22:49:53 2008 +0200
     1.3 @@ -144,8 +144,8 @@
     1.4    commands this is a plain macro with a single argument, e.g.\
     1.5    @{verbatim "\\isamarkupchapter{"}@{text "\<dots>"}@{verbatim "}"} for
     1.6    @{command "chapter"}.  The @{command "text"} markup results in a
     1.7 -  {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"}~@{text
     1.8 -  "\<dots>"}~@{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"}
     1.9 +  {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"} @{text
    1.10 +  "\<dots>"} @{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"}
    1.11    causes the text to be inserted directly into the {\LaTeX} source.
    1.12  
    1.13    \medskip Additional markup commands are available for proofs (see
    1.14 @@ -338,7 +338,7 @@
    1.15    \item [@{command "constdefs"}] provides a streamlined combination of
    1.16    constants declarations and definitions: type-inference takes care of
    1.17    the most general typing of the given specification (the optional
    1.18 -  type constraint may refer to type-inference dummies ``@{verbatim
    1.19 +  type constraint may refer to type-inference dummies ``@{text
    1.20    _}'' as usual).  The resulting type declaration needs to agree with
    1.21    that of the specification; overloading is \emph{not} supported here!
    1.22    
    1.23 @@ -652,8 +652,8 @@
    1.24    \end{matharray}
    1.25  
    1.26    The oracle interface promotes a given ML function @{ML_text
    1.27 -  "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some type
    1.28 -  @{ML_text T} given by the user.  This acts like an infinitary
    1.29 +  "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some
    1.30 +  type @{ML_text T} given by the user.  This acts like an infinitary
    1.31    specification of axioms -- there is no internal check of the
    1.32    correctness of the results!  The inference kernel records oracle
    1.33    invocations within the internal derivation object of theorems, and
    1.34 @@ -668,10 +668,11 @@
    1.35    \begin{descr}
    1.36  
    1.37    \item [@{command "oracle"}~@{text "name (type) = text"}] turns the
    1.38 -  given ML expression @{text "text"} of type @{ML_text "{theory
    1.39 -  ->"}~@{text "type"}~@{ML_text "-> term"} into an ML function
    1.40 -  @{ML_text name} of type @{ML_text "{theory ->"}~@{text
    1.41 -  "type"}~@{ML_text "-> thm"}.
    1.42 +  given ML expression @{text "text"} of type
    1.43 +  @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an
    1.44 +  ML function of type
    1.45 +  @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is
    1.46 +  bound to the global identifier @{ML_text name}.
    1.47  
    1.48    \end{descr}
    1.49  *}
    1.50 @@ -750,7 +751,7 @@
    1.51    assumptions.  The former closely correspond to Skolem constants, or
    1.52    meta-level universal quantification as provided by the Isabelle/Pure
    1.53    logical framework.  Introducing some \emph{arbitrary, but fixed}
    1.54 -  variable via ``@{command "fix"}~@{text x} results in a local value
    1.55 +  variable via ``@{command "fix"}~@{text x}'' results in a local value
    1.56    that may be used in the subsequent proof as any other variable or
    1.57    constant.  Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
    1.58    the context will be universally closed wrt.\ @{text x} at the
    1.59 @@ -1138,7 +1139,7 @@
    1.60    context.  Thus @{text "qed"} may fail for two reasons: either @{text
    1.61    "m\<^sub>2"} fails, or the resulting rule does not fit to any
    1.62    pending goal\footnote{This includes any additional ``strong''
    1.63 -  assumptions as introduced by @{text "assume"}.} of the enclosing
    1.64 +  assumptions as introduced by @{command "assume"}.} of the enclosing
    1.65    context.  Debugging such a situation might involve temporarily
    1.66    changing @{command "show"} into @{command "have"}, or weakening the
    1.67    local context by replacing occurrences of @{command "assume"} by
    1.68 @@ -1224,8 +1225,8 @@
    1.69  
    1.70    \begin{descr}
    1.71    
    1.72 -  \item [``@{method "-"}''] does nothing but insert the forward
    1.73 -  chaining facts as premises into the goal.  Note that command
    1.74 +  \item [``@{method "-"}'' (minus)] does nothing but insert the
    1.75 +  forward chaining facts as premises into the goal.  Note that command
    1.76    @{command_ref "proof"} without any method actually performs a single
    1.77    reduction step using the @{method_ref rule} method; thus a plain
    1.78    \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
    1.79 @@ -1274,8 +1275,8 @@
    1.80    means to include the current @{fact prems} as well.
    1.81    
    1.82    Rules need to be classified as @{attribute intro}, @{attribute
    1.83 -  elim}, or @{attribute dest}; here the ``@{text "!"} indicator refers
    1.84 -  to ``safe'' rules, which may be applied aggressively (without
    1.85 +  elim}, or @{attribute dest}; here the ``@{text "!"}'' indicator
    1.86 +  refers to ``safe'' rules, which may be applied aggressively (without
    1.87    considering back-tracking later).  Rules declared with ``@{text
    1.88    "?"}'' are ignored in proof search (the single-step @{method rule}
    1.89    method still observes these).  An explicit weight annotation may be
    1.90 @@ -1299,24 +1300,24 @@
    1.91    theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
    1.92    (in parallel).  This corresponds to the @{ML "op MRS"} operation in
    1.93    ML, but note the reversed order.  Positions may be effectively
    1.94 -  skipped by including ``@{verbatim _}'' (underscore) as argument.
    1.95 +  skipped by including ``@{text _}'' (underscore) as argument.
    1.96    
    1.97    \item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
    1.98    positional instantiation of term variables.  The terms @{text
    1.99    "t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
   1.100 -  variables occurring in a theorem from left to right; ``@{verbatim
   1.101 +  variables occurring in a theorem from left to right; ``@{text
   1.102    _}'' (underscore) indicates to skip a position.  Arguments following
   1.103    a ``@{keyword "concl"}@{text ":"}'' specification refer to positions
   1.104    of the conclusion of a rule.
   1.105    
   1.106    \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
   1.107 -  \<AND> x\<^sub>n = t\<^sub>n"}] performs named instantiation of
   1.108 -  schematic type and term variables occurring in a theorem.  Schematic
   1.109 -  variables have to be specified on the left-hand side (e.g.\ @{text
   1.110 -  "?x1.3"}).  The question mark may be omitted if the variable name is
   1.111 -  a plain identifier without index.  As type instantiations are
   1.112 -  inferred from term instantiations, explicit type instantiations are
   1.113 -  seldom necessary.
   1.114 +  x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic
   1.115 +  type and term variables occurring in a theorem.  Schematic variables
   1.116 +  have to be specified on the left-hand side (e.g.\ @{text "?x1.3"}).
   1.117 +  The question mark may be omitted if the variable name is a plain
   1.118 +  identifier without index.  As type instantiations are inferred from
   1.119 +  term instantiations, explicit type instantiations are seldom
   1.120 +  necessary.
   1.121  
   1.122    \end{descr}
   1.123  *}
   1.124 @@ -1330,15 +1331,15 @@
   1.125      @{keyword_def "is"} & : & syntax \\
   1.126    \end{matharray}
   1.127  
   1.128 -  Abbreviations may be either bound by explicit @{command "let"}@{text
   1.129 -  "p \<equiv> t"} statements, or by annotating assumptions or goal statements
   1.130 -  with a list of patterns ``@{text "\<IS> p\<^sub>1 \<dots> p\<^sub>n"}''.
   1.131 -  In both cases, higher-order matching is invoked to bind
   1.132 -  extra-logical term variables, which may be either named schematic
   1.133 -  variables of the form @{text ?x}, or nameless dummies ``@{variable
   1.134 -  _}'' (underscore). Note that in the @{command "let"} form the
   1.135 -  patterns occur on the left-hand side, while the @{keyword "is"}
   1.136 -  patterns are in postfix position.
   1.137 +  Abbreviations may be either bound by explicit @{command
   1.138 +  "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
   1.139 +  goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
   1.140 +  p\<^sub>n)"}''.  In both cases, higher-order matching is invoked to
   1.141 +  bind extra-logical term variables, which may be either named
   1.142 +  schematic variables of the form @{text ?x}, or nameless dummies
   1.143 +  ``@{variable _}'' (underscore). Note that in the @{command "let"}
   1.144 +  form the patterns occur on the left-hand side, while the @{keyword
   1.145 +  "is"} patterns are in postfix position.
   1.146  
   1.147    Polymorphism of term bindings is handled in Hindley-Milner style,
   1.148    similar to ML.  Type variables referring to local assumptions or
   1.149 @@ -1366,10 +1367,10 @@
   1.150  
   1.151    \begin{descr}
   1.152  
   1.153 -  \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND>
   1.154 -  \<dots>p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns
   1.155 -  @{text "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order
   1.156 -  matching against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
   1.157 +  \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots>
   1.158 +  p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text
   1.159 +  "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order matching
   1.160 +  against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
   1.161  
   1.162    \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
   1.163    "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
   1.164 @@ -1612,8 +1613,8 @@
   1.165  
   1.166    \item [@{command "full_prf"}] is like @{command "prf"}, but displays
   1.167    the full proof term, i.e.\ also displays information omitted in the
   1.168 -  compact proof term, which is denoted by ``@{verbatim _}''
   1.169 -  placeholders there.
   1.170 +  compact proof term, which is denoted by ``@{text _}'' placeholders
   1.171 +  there.
   1.172  
   1.173    \end{descr}
   1.174  
   1.175 @@ -1700,7 +1701,7 @@
   1.176    rules whose left-hand side matches the given term.  The criterion
   1.177    term @{text t} selects all theorems that contain the pattern @{text
   1.178    t} -- as usual, patterns may contain occurrences of the dummy
   1.179 -  ``@{verbatim _}'', schematic variables, and type constraints.
   1.180 +  ``@{text _}'', schematic variables, and type constraints.
   1.181    
   1.182    Criteria can be preceded by ``@{text "-"}'' to select theorems that
   1.183    do \emph{not} match. Note that giving the empty list of criteria

     2.1 --- a/doc-src/IsarRef/Thy/syntax.thy	Fri May 02 22:48:51 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/syntax.thy	Fri May 02 22:49:53 2008 +0200
     2.3 @@ -240,8 +240,8 @@
     2.4    \end{rail}
     2.5  
     2.6    Positional instantiations are indicated by giving a sequence of
     2.7 -  terms, or the placeholder ``@{verbatim _}'' (underscore), which
     2.8 -  means to skip a position.
     2.9 +  terms, or the placeholder ``@{text _}'' (underscore), which means to
    2.10 +  skip a position.
    2.11  
    2.12    \indexoutertoken{inst}\indexoutertoken{insts}
    2.13    \begin{rail}
    2.14 @@ -289,8 +289,8 @@
    2.15  
    2.16    Here the \railtok{string} specifications refer to the actual mixfix
    2.17    template (see also \cite{isabelle-ref}), which may include literal
    2.18 -  text, spacing, blocks, and arguments (denoted by ``@{verbatim _}'');
    2.19 -  the special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'')
    2.20 +  text, spacing, blocks, and arguments (denoted by ``@{text _}''); the
    2.21 +  special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'')
    2.22    represents an index argument that specifies an implicit structure
    2.23    reference (see also \secref{sec:locale}).  Infix and binder
    2.24    declarations provide common abbreviations for particular mixfix
    2.25 @@ -606,7 +606,7 @@
    2.26    \item [@{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"}] is like @{text
    2.27    "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but displays the full proof terms,
    2.28    i.e.\ also displays information omitted in the compact proof term,
    2.29 -  which is denoted by ``@{verbatim _}'' placeholders there.
    2.30 +  which is denoted by ``@{text _}'' placeholders there.
    2.31    
    2.32    \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
    2.33    "@{ML_struct s}"}] check text @{text s} as ML value, type, and