# HG changeset patch # User wenzelm # Date 1209761393 -7200 # Node ID 134529bc72dbb64bb17ae38771221e231c14fc3e # Parent 030db8c8b79dd27dabb23953a7c9fc9fe3eea9dd misc tuning; diff -r 030db8c8b79d -r 134529bc72db doc-src/IsarRef/Thy/pure.thy --- a/doc-src/IsarRef/Thy/pure.thy Fri May 02 22:48:51 2008 +0200 +++ b/doc-src/IsarRef/Thy/pure.thy Fri May 02 22:49:53 2008 +0200 @@ -144,8 +144,8 @@ commands this is a plain macro with a single argument, e.g.\ @{verbatim "\\isamarkupchapter{"}@{text "\"}@{verbatim "}"} for @{command "chapter"}. The @{command "text"} markup results in a - {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"}~@{text - "\"}~@{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"} + {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"} @{text + "\"} @{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"} causes the text to be inserted directly into the {\LaTeX} source. \medskip Additional markup commands are available for proofs (see @@ -338,7 +338,7 @@ \item [@{command "constdefs"}] provides a streamlined combination of constants declarations and definitions: type-inference takes care of the most general typing of the given specification (the optional - type constraint may refer to type-inference dummies ``@{verbatim + type constraint may refer to type-inference dummies ``@{text _}'' as usual). The resulting type declaration needs to agree with that of the specification; overloading is \emph{not} supported here! @@ -652,8 +652,8 @@ \end{matharray} The oracle interface promotes a given ML function @{ML_text - "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some type - @{ML_text T} given by the user. This acts like an infinitary + "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some + type @{ML_text T} given by the user. This acts like an infinitary specification of axioms -- there is no internal check of the correctness of the results! The inference kernel records oracle invocations within the internal derivation object of theorems, and @@ -668,10 +668,11 @@ \begin{descr} \item [@{command "oracle"}~@{text "name (type) = text"}] turns the - given ML expression @{text "text"} of type @{ML_text "{theory - ->"}~@{text "type"}~@{ML_text "-> term"} into an ML function - @{ML_text name} of type @{ML_text "{theory ->"}~@{text - "type"}~@{ML_text "-> thm"}. + given ML expression @{text "text"} of type + @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an + ML function of type + @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is + bound to the global identifier @{ML_text name}. \end{descr} *} @@ -750,7 +751,7 @@ assumptions. The former closely correspond to Skolem constants, or meta-level universal quantification as provided by the Isabelle/Pure logical framework. Introducing some \emph{arbitrary, but fixed} - variable via ``@{command "fix"}~@{text x} results in a local value + variable via ``@{command "fix"}~@{text x}'' results in a local value that may be used in the subsequent proof as any other variable or constant. Furthermore, any result @{text "\ \[x]"} exported from the context will be universally closed wrt.\ @{text x} at the @@ -1138,7 +1139,7 @@ context. Thus @{text "qed"} may fail for two reasons: either @{text "m\<^sub>2"} fails, or the resulting rule does not fit to any pending goal\footnote{This includes any additional ``strong'' - assumptions as introduced by @{text "assume"}.} of the enclosing + assumptions as introduced by @{command "assume"}.} of the enclosing context. Debugging such a situation might involve temporarily changing @{command "show"} into @{command "have"}, or weakening the local context by replacing occurrences of @{command "assume"} by @@ -1224,8 +1225,8 @@ \begin{descr} - \item [``@{method "-"}''] does nothing but insert the forward - chaining facts as premises into the goal. Note that command + \item [``@{method "-"}'' (minus)] does nothing but insert the + forward chaining facts as premises into the goal. Note that command @{command_ref "proof"} without any method actually performs a single reduction step using the @{method_ref rule} method; thus a plain \emph{do-nothing} proof step would be ``@{command "proof"}~@{text @@ -1274,8 +1275,8 @@ means to include the current @{fact prems} as well. Rules need to be classified as @{attribute intro}, @{attribute - elim}, or @{attribute dest}; here the ``@{text "!"} indicator refers - to ``safe'' rules, which may be applied aggressively (without + elim}, or @{attribute dest}; here the ``@{text "!"}'' indicator + refers to ``safe'' rules, which may be applied aggressively (without considering back-tracking later). Rules declared with ``@{text "?"}'' are ignored in proof search (the single-step @{method rule} method still observes these). An explicit weight annotation may be @@ -1299,24 +1300,24 @@ theorem to all of the given rules @{text "a\<^sub>1, \, a\<^sub>n"} (in parallel). This corresponds to the @{ML "op MRS"} operation in ML, but note the reversed order. Positions may be effectively - skipped by including ``@{verbatim _}'' (underscore) as argument. + skipped by including ``@{text _}'' (underscore) as argument. \item [@{attribute of}~@{text "t\<^sub>1 \ t\<^sub>n"}] performs positional instantiation of term variables. The terms @{text "t\<^sub>1, \, t\<^sub>n"} are substituted for any schematic - variables occurring in a theorem from left to right; ``@{verbatim + variables occurring in a theorem from left to right; ``@{text _}'' (underscore) indicates to skip a position. Arguments following a ``@{keyword "concl"}@{text ":"}'' specification refer to positions of the conclusion of a rule. \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \ \ - \ x\<^sub>n = t\<^sub>n"}] performs named instantiation of - schematic type and term variables occurring in a theorem. Schematic - variables have to be specified on the left-hand side (e.g.\ @{text - "?x1.3"}). The question mark may be omitted if the variable name is - a plain identifier without index. As type instantiations are - inferred from term instantiations, explicit type instantiations are - seldom necessary. + x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic + type and term variables occurring in a theorem. Schematic variables + have to be specified on the left-hand side (e.g.\ @{text "?x1.3"}). + The question mark may be omitted if the variable name is a plain + identifier without index. As type instantiations are inferred from + term instantiations, explicit type instantiations are seldom + necessary. \end{descr} *} @@ -1330,15 +1331,15 @@ @{keyword_def "is"} & : & syntax \\ \end{matharray} - Abbreviations may be either bound by explicit @{command "let"}@{text - "p \ t"} statements, or by annotating assumptions or goal statements - with a list of patterns ``@{text "\ p\<^sub>1 \ p\<^sub>n"}''. - In both cases, higher-order matching is invoked to bind - extra-logical term variables, which may be either named schematic - variables of the form @{text ?x}, or nameless dummies ``@{variable - _}'' (underscore). Note that in the @{command "let"} form the - patterns occur on the left-hand side, while the @{keyword "is"} - patterns are in postfix position. + Abbreviations may be either bound by explicit @{command + "let"}~@{text "p \ t"} statements, or by annotating assumptions or + goal statements with a list of patterns ``@{text "(\ p\<^sub>1 \ + p\<^sub>n)"}''. In both cases, higher-order matching is invoked to + bind extra-logical term variables, which may be either named + schematic variables of the form @{text ?x}, or nameless dummies + ``@{variable _}'' (underscore). Note that in the @{command "let"} + form the patterns occur on the left-hand side, while the @{keyword + "is"} patterns are in postfix position. Polymorphism of term bindings is handled in Hindley-Milner style, similar to ML. Type variables referring to local assumptions or @@ -1366,10 +1367,10 @@ \begin{descr} - \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \ - \p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns - @{text "p\<^sub>1, \, p\<^sub>n"} by simultaneous higher-order - matching against terms @{text "t\<^sub>1, \, t\<^sub>n"}. + \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \ \ + p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text + "p\<^sub>1, \, p\<^sub>n"} by simultaneous higher-order matching + against terms @{text "t\<^sub>1, \, t\<^sub>n"}. \item [@{text "(\ p\<^sub>1 \ p\<^sub>n)"}] resembles @{command "let"}, but matches @{text "p\<^sub>1, \, p\<^sub>n"} against the @@ -1612,8 +1613,8 @@ \item [@{command "full_prf"}] is like @{command "prf"}, but displays the full proof term, i.e.\ also displays information omitted in the - compact proof term, which is denoted by ``@{verbatim _}'' - placeholders there. + compact proof term, which is denoted by ``@{text _}'' placeholders + there. \end{descr} @@ -1700,7 +1701,7 @@ rules whose left-hand side matches the given term. The criterion term @{text t} selects all theorems that contain the pattern @{text t} -- as usual, patterns may contain occurrences of the dummy - ``@{verbatim _}'', schematic variables, and type constraints. + ``@{text _}'', schematic variables, and type constraints. Criteria can be preceded by ``@{text "-"}'' to select theorems that do \emph{not} match. Note that giving the empty list of criteria diff -r 030db8c8b79d -r 134529bc72db doc-src/IsarRef/Thy/syntax.thy --- a/doc-src/IsarRef/Thy/syntax.thy Fri May 02 22:48:51 2008 +0200 +++ b/doc-src/IsarRef/Thy/syntax.thy Fri May 02 22:49:53 2008 +0200 @@ -240,8 +240,8 @@ \end{rail} Positional instantiations are indicated by giving a sequence of - terms, or the placeholder ``@{verbatim _}'' (underscore), which - means to skip a position. + terms, or the placeholder ``@{text _}'' (underscore), which means to + skip a position. \indexoutertoken{inst}\indexoutertoken{insts} \begin{rail} @@ -289,8 +289,8 @@ Here the \railtok{string} specifications refer to the actual mixfix template (see also \cite{isabelle-ref}), which may include literal - text, spacing, blocks, and arguments (denoted by ``@{verbatim _}''); - the special symbol ``@{verbatim "\"}'' (printed as ``@{text "\"}'') + text, spacing, blocks, and arguments (denoted by ``@{text _}''); the + special symbol ``@{verbatim "\"}'' (printed as ``@{text "\"}'') represents an index argument that specifies an implicit structure reference (see also \secref{sec:locale}). Infix and binder declarations provide common abbreviations for particular mixfix @@ -606,7 +606,7 @@ \item [@{text "@{full_prf a\<^sub>1 \ a\<^sub>n}"}] is like @{text "@{prf a\<^sub>1 \ a\<^sub>n}"}, but displays the full proof terms, i.e.\ also displays information omitted in the compact proof term, - which is denoted by ``@{verbatim _}'' placeholders there. + which is denoted by ``@{text _}'' placeholders there. \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text "@{ML_struct s}"}] check text @{text s} as ML value, type, and