src/Doc/Isar_Ref/Outer_Syntax.thy
changeset 61493 0debd22f0c0e
parent 61477 e467ae7aa808
child 61494 63b18f758874
     1.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue Oct 20 23:03:46 2015 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue Oct 20 23:53:40 2015 +0200
     1.3 @@ -39,8 +39,8 @@
     1.4  
     1.5  text \<open>
     1.6    \begin{matharray}{rcl}
     1.7 -    @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     1.8 -    @{command_def "help"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     1.9 +    @{command_def "print_commands"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
    1.10 +    @{command_def "help"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
    1.11    \end{matharray}
    1.12  
    1.13    @{rail \<open>
    1.14 @@ -50,7 +50,7 @@
    1.15    \<^descr> @{command "print_commands"} prints all outer syntax keywords
    1.16    and commands.
    1.17  
    1.18 -  \<^descr> @{command "help"}~@{text "pats"} retrieves outer syntax
    1.19 +  \<^descr> @{command "help"}~\<open>pats\<close> retrieves outer syntax
    1.20    commands according to the specified name patterns.
    1.21  \<close>
    1.22  
    1.23 @@ -101,50 +101,49 @@
    1.24  
    1.25    \begin{center}
    1.26    \begin{supertabular}{rcl}
    1.27 -    @{syntax_def ident} & = & @{text "letter (subscript\<^sup>? quasiletter)\<^sup>*"} \\
    1.28 -    @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
    1.29 -    @{syntax_def symident} & = & @{text "sym\<^sup>+  |  "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
    1.30 -    @{syntax_def nat} & = & @{text "digit\<^sup>+"} \\
    1.31 -    @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
    1.32 -    @{syntax_def var} & = & @{verbatim "?"}@{text "ident  |  "}@{verbatim "?"}@{text ident}@{verbatim "."}@{text nat} \\
    1.33 -    @{syntax_def typefree} & = & @{verbatim "'"}@{text ident} \\
    1.34 -    @{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree  |  "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\
    1.35 -    @{syntax_def string} & = & @{verbatim \<open>"\<close>} @{text "\<dots>"} @{verbatim \<open>"\<close>} \\
    1.36 -    @{syntax_def altstring} & = & @{verbatim "`"} @{text "\<dots>"} @{verbatim "`"} \\
    1.37 -    @{syntax_def cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
    1.38 -    @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*}"} \\[1ex]
    1.39 +    @{syntax_def ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
    1.40 +    @{syntax_def longident} & = & \<open>ident(\<close>@{verbatim "."}\<open>ident)\<^sup>+\<close> \\
    1.41 +    @{syntax_def symident} & = & \<open>sym\<^sup>+  |  \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>ident\<close>@{verbatim ">"} \\
    1.42 +    @{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\
    1.43 +    @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}\<open>  |  \<close>@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
    1.44 +    @{syntax_def var} & = & @{verbatim "?"}\<open>ident  |  \<close>@{verbatim "?"}\<open>ident\<close>@{verbatim "."}\<open>nat\<close> \\
    1.45 +    @{syntax_def typefree} & = & @{verbatim "'"}\<open>ident\<close> \\
    1.46 +    @{syntax_def typevar} & = & @{verbatim "?"}\<open>typefree  |  \<close>@{verbatim "?"}\<open>typefree\<close>@{verbatim "."}\<open>nat\<close> \\
    1.47 +    @{syntax_def string} & = & @{verbatim \<open>"\<close>} \<open>\<dots>\<close> @{verbatim \<open>"\<close>} \\
    1.48 +    @{syntax_def altstring} & = & @{verbatim "`"} \<open>\<dots>\<close> @{verbatim "`"} \\
    1.49 +    @{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
    1.50 +    @{syntax_def verbatim} & = & @{verbatim "{*"} \<open>\<dots>\<close> @{verbatim "*}"} \\[1ex]
    1.51  
    1.52 -    @{text letter} & = & @{text "latin  |  "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  |  "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  |  greek  |"} \\
    1.53 -    @{text subscript} & = & @{verbatim "\<^sub>"} \\
    1.54 -    @{text quasiletter} & = & @{text "letter  |  digit  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "'"} \\
    1.55 -    @{text latin} & = & @{verbatim a}@{text "  | \<dots> |  "}@{verbatim z}@{text "  |  "}@{verbatim A}@{text "  |  \<dots> |  "}@{verbatim Z} \\
    1.56 -    @{text digit} & = & @{verbatim "0"}@{text "  |  \<dots> |  "}@{verbatim "9"} \\
    1.57 -    @{text sym} & = & @{verbatim "!"}@{text "  |  "}@{verbatim "#"}@{text "  |  "}@{verbatim "$"}@{text "  |  "}@{verbatim "%"}@{text "  |  "}@{verbatim "&"}@{text "  |  "}@{verbatim "*"}@{text "  |  "}@{verbatim "+"}@{text "  |  "}@{verbatim "-"}@{text "  |  "}@{verbatim "/"}@{text "  |"} \\
    1.58 -    & & @{verbatim "<"}@{text "  |  "}@{verbatim "="}@{text "  |  "}@{verbatim ">"}@{text "  |  "}@{verbatim "?"}@{text "  |  "}@{verbatim "@"}@{text "  |  "}@{verbatim "^"}@{text "  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "|"}@{text "  |  "}@{verbatim "~"} \\
    1.59 -    @{text greek} & = & @{verbatim "\<alpha>"}@{text "  |  "}@{verbatim "\<beta>"}@{text "  |  "}@{verbatim "\<gamma>"}@{text "  |  "}@{verbatim "\<delta>"}@{text "  |"} \\
    1.60 -          &   & @{verbatim "\<epsilon>"}@{text "  |  "}@{verbatim "\<zeta>"}@{text "  |  "}@{verbatim "\<eta>"}@{text "  |  "}@{verbatim "\<theta>"}@{text "  |"} \\
    1.61 -          &   & @{verbatim "\<iota>"}@{text "  |  "}@{verbatim "\<kappa>"}@{text "  |  "}@{verbatim "\<mu>"}@{text "  |  "}@{verbatim "\<nu>"}@{text "  |"} \\
    1.62 -          &   & @{verbatim "\<xi>"}@{text "  |  "}@{verbatim "\<pi>"}@{text "  |  "}@{verbatim "\<rho>"}@{text "  |  "}@{verbatim "\<sigma>"}@{text "  |  "}@{verbatim "\<tau>"}@{text "  |"} \\
    1.63 -          &   & @{verbatim "\<upsilon>"}@{text "  |  "}@{verbatim "\<phi>"}@{text "  |  "}@{verbatim "\<chi>"}@{text "  |  "}@{verbatim "\<psi>"}@{text "  |"} \\
    1.64 -          &   & @{verbatim "\<omega>"}@{text "  |  "}@{verbatim "\<Gamma>"}@{text "  |  "}@{verbatim "\<Delta>"}@{text "  |  "}@{verbatim "\<Theta>"}@{text "  |"} \\
    1.65 -          &   & @{verbatim "\<Lambda>"}@{text "  |  "}@{verbatim "\<Xi>"}@{text "  |  "}@{verbatim "\<Pi>"}@{text "  |  "}@{verbatim "\<Sigma>"}@{text "  |"} \\
    1.66 -          &   & @{verbatim "\<Upsilon>"}@{text "  |  "}@{verbatim "\<Phi>"}@{text "  |  "}@{verbatim "\<Psi>"}@{text "  |  "}@{verbatim "\<Omega>"} \\
    1.67 +    \<open>letter\<close> & = & \<open>latin  |  \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin\<close>@{verbatim ">"}\<open>  |  \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin latin\<close>@{verbatim ">"}\<open>  |  greek  |\<close> \\
    1.68 +    \<open>subscript\<close> & = & @{verbatim "\<^sub>"} \\
    1.69 +    \<open>quasiletter\<close> & = & \<open>letter  |  digit  |  \<close>@{verbatim "_"}\<open>  |  \<close>@{verbatim "'"} \\
    1.70 +    \<open>latin\<close> & = & @{verbatim a}\<open>  | \<dots> |  \<close>@{verbatim z}\<open>  |  \<close>@{verbatim A}\<open>  |  \<dots> |  \<close>@{verbatim Z} \\
    1.71 +    \<open>digit\<close> & = & @{verbatim "0"}\<open>  |  \<dots> |  \<close>@{verbatim "9"} \\
    1.72 +    \<open>sym\<close> & = & @{verbatim "!"}\<open>  |  \<close>@{verbatim "#"}\<open>  |  \<close>@{verbatim "$"}\<open>  |  \<close>@{verbatim "%"}\<open>  |  \<close>@{verbatim "&"}\<open>  |  \<close>@{verbatim "*"}\<open>  |  \<close>@{verbatim "+"}\<open>  |  \<close>@{verbatim "-"}\<open>  |  \<close>@{verbatim "/"}\<open>  |\<close> \\
    1.73 +    & & @{verbatim "<"}\<open>  |  \<close>@{verbatim "="}\<open>  |  \<close>@{verbatim ">"}\<open>  |  \<close>@{verbatim "?"}\<open>  |  \<close>@{verbatim "@"}\<open>  |  \<close>@{verbatim "^"}\<open>  |  \<close>@{verbatim "_"}\<open>  |  \<close>@{verbatim "|"}\<open>  |  \<close>@{verbatim "~"} \\
    1.74 +    \<open>greek\<close> & = & @{verbatim "\<alpha>"}\<open>  |  \<close>@{verbatim "\<beta>"}\<open>  |  \<close>@{verbatim "\<gamma>"}\<open>  |  \<close>@{verbatim "\<delta>"}\<open>  |\<close> \\
    1.75 +          &   & @{verbatim "\<epsilon>"}\<open>  |  \<close>@{verbatim "\<zeta>"}\<open>  |  \<close>@{verbatim "\<eta>"}\<open>  |  \<close>@{verbatim "\<theta>"}\<open>  |\<close> \\
    1.76 +          &   & @{verbatim "\<iota>"}\<open>  |  \<close>@{verbatim "\<kappa>"}\<open>  |  \<close>@{verbatim "\<mu>"}\<open>  |  \<close>@{verbatim "\<nu>"}\<open>  |\<close> \\
    1.77 +          &   & @{verbatim "\<xi>"}\<open>  |  \<close>@{verbatim "\<pi>"}\<open>  |  \<close>@{verbatim "\<rho>"}\<open>  |  \<close>@{verbatim "\<sigma>"}\<open>  |  \<close>@{verbatim "\<tau>"}\<open>  |\<close> \\
    1.78 +          &   & @{verbatim "\<upsilon>"}\<open>  |  \<close>@{verbatim "\<phi>"}\<open>  |  \<close>@{verbatim "\<chi>"}\<open>  |  \<close>@{verbatim "\<psi>"}\<open>  |\<close> \\
    1.79 +          &   & @{verbatim "\<omega>"}\<open>  |  \<close>@{verbatim "\<Gamma>"}\<open>  |  \<close>@{verbatim "\<Delta>"}\<open>  |  \<close>@{verbatim "\<Theta>"}\<open>  |\<close> \\
    1.80 +          &   & @{verbatim "\<Lambda>"}\<open>  |  \<close>@{verbatim "\<Xi>"}\<open>  |  \<close>@{verbatim "\<Pi>"}\<open>  |  \<close>@{verbatim "\<Sigma>"}\<open>  |\<close> \\
    1.81 +          &   & @{verbatim "\<Upsilon>"}\<open>  |  \<close>@{verbatim "\<Phi>"}\<open>  |  \<close>@{verbatim "\<Psi>"}\<open>  |  \<close>@{verbatim "\<Omega>"} \\
    1.82    \end{supertabular}
    1.83    \end{center}
    1.84  
    1.85    A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown,
    1.86    which is internally a pair of base name and index (ML type @{ML_type
    1.87    indexname}).  These components are either separated by a dot as in
    1.88 -  @{text "?x.1"} or @{text "?x7.3"} or run together as in @{text
    1.89 -  "?x1"}.  The latter form is possible if the base name does not end
    1.90 +  \<open>?x.1\<close> or \<open>?x7.3\<close> or run together as in \<open>?x1\<close>.  The latter form is possible if the base name does not end
    1.91    with digits.  If the index is 0, it may be dropped altogether:
    1.92 -  @{text "?x"} and @{text "?x0"} and @{text "?x.0"} all refer to the
    1.93 -  same unknown, with basename @{text "x"} and index 0.
    1.94 +  \<open>?x\<close> and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the
    1.95 +  same unknown, with basename \<open>x\<close> and index 0.
    1.96  
    1.97    The syntax of @{syntax_ref string} admits any characters, including
    1.98    newlines; ``@{verbatim \<open>"\<close>}'' (double-quote) and ``@{verbatim \<open>\\<close>}''
    1.99    (backslash) need to be escaped by a backslash; arbitrary
   1.100 -  character codes may be specified as ``@{verbatim \<open>\\<close>}@{text ddd}'',
   1.101 +  character codes may be specified as ``@{verbatim \<open>\\<close>}\<open>ddd\<close>'',
   1.102    with three decimal digits.  Alternative strings according to
   1.103    @{syntax_ref altstring} are analogous, using single back-quotes
   1.104    instead.
   1.105 @@ -155,24 +154,23 @@
   1.106    do not have this limitation.
   1.107  
   1.108    A @{syntax_ref cartouche} consists of arbitrary text, with properly
   1.109 -  balanced blocks of ``@{verbatim "\<open>"}~@{text "\<dots>"}~@{verbatim
   1.110 +  balanced blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim
   1.111    "\<close>"}''.  Note that the rendering of cartouche delimiters is
   1.112 -  usually like this: ``@{text "\<open> \<dots> \<close>"}''.
   1.113 +  usually like this: ``\<open>\<open> \<dots> \<close>\<close>''.
   1.114  
   1.115 -  Source comments take the form @{verbatim "(*"}~@{text
   1.116 -  "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface
   1.117 +  Source comments take the form @{verbatim "(*"}~\<open>\<dots>\<close>~@{verbatim "*)"} and may be nested, although the user-interface
   1.118    might prevent this.  Note that this form indicates source comments
   1.119    only, which are stripped after lexical analysis of the input.  The
   1.120    Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are
   1.121    considered as part of the text (see \secref{sec:comments}).
   1.122  
   1.123 -  Common mathematical symbols such as @{text \<forall>} are represented in
   1.124 +  Common mathematical symbols such as \<open>\<forall>\<close> are represented in
   1.125    Isabelle as @{verbatim \<forall>}.  There are infinitely many Isabelle
   1.126    symbols like this, although proper presentation is left to front-end
   1.127    tools such as {\LaTeX} or Isabelle/jEdit.  A list of
   1.128    predefined Isabelle symbols that work well with these tools is given
   1.129    in \appref{app:symbols}.  Note that @{verbatim "\<lambda>"} does not belong
   1.130 -  to the @{text letter} category, since it is already used differently
   1.131 +  to the \<open>letter\<close> category, since it is already used differently
   1.132    in the Pure term language.\<close>
   1.133  
   1.134  
   1.135 @@ -226,8 +224,8 @@
   1.136  subsection \<open>Comments \label{sec:comments}\<close>
   1.137  
   1.138  text \<open>Large chunks of plain @{syntax text} are usually given @{syntax
   1.139 -  verbatim}, i.e.\ enclosed in @{verbatim "{*"}~@{text "\<dots>"}~@{verbatim "*}"},
   1.140 -  or as @{syntax cartouche} @{text "\<open>\<dots>\<close>"}. For convenience, any of the
   1.141 +  verbatim}, i.e.\ enclosed in @{verbatim "{*"}~\<open>\<dots>\<close>~@{verbatim "*}"},
   1.142 +  or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For convenience, any of the
   1.143    smaller text units conforming to @{syntax nameref} are admitted as well. A
   1.144    marginal @{syntax comment} is of the form @{verbatim "--"}~@{syntax text}.
   1.145    Any number of these may occur within Isabelle/Isar commands.
   1.146 @@ -244,8 +242,8 @@
   1.147  
   1.148  text \<open>
   1.149    Classes are specified by plain names.  Sorts have a very simple
   1.150 -  inner syntax, which is either a single class name @{text c} or a
   1.151 -  list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the
   1.152 +  inner syntax, which is either a single class name \<open>c\<close> or a
   1.153 +  list \<open>{c\<^sub>1, \<dots>, c\<^sub>n}\<close> referring to the
   1.154    intersection of these classes.  The syntax of type arities is given
   1.155    directly at the outer level.
   1.156  
   1.157 @@ -270,8 +268,7 @@
   1.158    liberal convention is adopted: quotes may be omitted for any type or
   1.159    term that is already atomic at the outer level.  For example, one
   1.160    may just write @{verbatim x} instead of quoted @{verbatim \<open>"x"\<close>}.
   1.161 -  Note that symbolic identifiers (e.g.\ @{verbatim "++"} or @{text
   1.162 -  "\<forall>"} are available as well, provided these have not been superseded
   1.163 +  Note that symbolic identifiers (e.g.\ @{verbatim "++"} or \<open>\<forall>\<close> are available as well, provided these have not been superseded
   1.164    by commands or other keywords already (such as @{verbatim "="} or
   1.165    @{verbatim "+"}).
   1.166  
   1.167 @@ -285,7 +282,7 @@
   1.168    \<close>}
   1.169  
   1.170    Positional instantiations are specified as a sequence of terms, or the
   1.171 -  placeholder ``@{text _}'' (underscore), which means to skip a position.
   1.172 +  placeholder ``\<open>_\<close>'' (underscore), which means to skip a position.
   1.173  
   1.174    @{rail \<open>
   1.175      @{syntax_def inst}: '_' | @{syntax term}
   1.176 @@ -293,8 +290,8 @@
   1.177      @{syntax_def insts}: (@{syntax inst} *)
   1.178    \<close>}
   1.179  
   1.180 -  Named instantiations are specified as pairs of assignments @{text "v =
   1.181 -  t"}, which refer to schematic variables in some theorem that is
   1.182 +  Named instantiations are specified as pairs of assignments \<open>v =
   1.183 +  t\<close>, which refer to schematic variables in some theorem that is
   1.184    instantiated. Both type and terms instantiations are admitted, and
   1.185    distinguished by the usual syntax of variable names.
   1.186  
   1.187 @@ -326,7 +323,7 @@
   1.188  
   1.189  text \<open>Wherever explicit propositions (or term fragments) occur in a
   1.190    proof text, casual binding of schematic term variables may be given
   1.191 -  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}''.
   1.192 +  specified via patterns of the form ``\<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close>''.
   1.193    This works both for @{syntax term} and @{syntax prop}.
   1.194  
   1.195    @{rail \<open>
   1.196 @@ -336,8 +333,8 @@
   1.197    \<close>}
   1.198  
   1.199    \<^medskip>
   1.200 -  Declarations of local variables @{text "x :: \<tau>"} and
   1.201 -  logical propositions @{text "a : \<phi>"} represent different views on
   1.202 +  Declarations of local variables \<open>x :: \<tau>\<close> and
   1.203 +  logical propositions \<open>a : \<phi>\<close> represent different views on
   1.204    the same principle of introducing a local scope.  In practice, one
   1.205    may usually omit the typing of @{syntax vars} (due to
   1.206    type-inference), and the naming of propositions (due to implicit
   1.207 @@ -352,8 +349,8 @@
   1.208  
   1.209    The treatment of multiple declarations corresponds to the
   1.210    complementary focus of @{syntax vars} versus @{syntax props}.  In
   1.211 -  ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}'' the typing refers to all variables, while
   1.212 -  in @{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} the naming refers to all propositions
   1.213 +  ``\<open>x\<^sub>1 \<dots> x\<^sub>n :: \<tau>\<close>'' the typing refers to all variables, while
   1.214 +  in \<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> the naming refers to all propositions
   1.215    collectively.  Isar language elements that refer to @{syntax vars}
   1.216    or @{syntax props} typically admit separate typings or namings via
   1.217    another level of iteration, with explicit @{keyword_ref "and"}
   1.218 @@ -369,7 +366,7 @@
   1.219  
   1.220    The category @{syntax "fixes"} is a richer variant of @{syntax vars}: it
   1.221    admits specification of mixfix syntax for the entities that are introduced
   1.222 -  into the context. An optional suffix ``@{keyword "for"}~@{text "fixes"}''
   1.223 +  into the context. An optional suffix ``@{keyword "for"}~\<open>fixes\<close>''
   1.224    is admitted in many situations to indicate a so-called ``eigen-context''
   1.225    of a formal element: the result will be exported and thus generalized over
   1.226    the given variables.\<close>
   1.227 @@ -406,13 +403,13 @@
   1.228  
   1.229    There are three forms of theorem references:
   1.230  
   1.231 -  \<^enum> named facts @{text "a"},
   1.232 +  \<^enum> named facts \<open>a\<close>,
   1.233  
   1.234 -  \<^enum> selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
   1.235 +  \<^enum> selections from named facts \<open>a(i)\<close> or \<open>a(j - k)\<close>,
   1.236  
   1.237    \<^enum> literal fact propositions using token syntax @{syntax_ref altstring}
   1.238 -  @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} or @{syntax_ref cartouche}
   1.239 -  @{text "\<open>\<phi>\<close>"} (see also method @{method_ref fact}).
   1.240 +  @{verbatim "`"}\<open>\<phi>\<close>@{verbatim "`"} or @{syntax_ref cartouche}
   1.241 +  \<open>\<open>\<phi>\<close>\<close> (see also method @{method_ref fact}).
   1.242  
   1.243  
   1.244    Any kind of theorem specification may include lists of attributes
   1.245 @@ -421,8 +418,7 @@
   1.246    not stored within the theorem database of the theory or proof
   1.247    context, but any given attributes are applied nonetheless.
   1.248  
   1.249 -  An extra pair of brackets around attributes (like ``@{text
   1.250 -  "[[simproc a]]"}'') abbreviates a theorem reference involving an
   1.251 +  An extra pair of brackets around attributes (like ``\<open>[[simproc a]]\<close>'') abbreviates a theorem reference involving an
   1.252    internal dummy fact, which will be ignored later on.  So only the
   1.253    effect of the attribute on the background context will persist.
   1.254    This form of in-place declarations is particularly useful with
   1.255 @@ -454,17 +450,17 @@
   1.256  
   1.257  text \<open>
   1.258    \begin{matharray}{rcl}
   1.259 -    @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.260 -    @{command_def "print_definitions"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.261 -    @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.262 -    @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.263 -    @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.264 -    @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.265 -    @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.266 -    @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.267 -    @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.268 -    @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.269 -    @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.270 +    @{command_def "print_theory"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.271 +    @{command_def "print_definitions"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.272 +    @{command_def "print_methods"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.273 +    @{command_def "print_attributes"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.274 +    @{command_def "print_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.275 +    @{command_def "find_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.276 +    @{command_def "find_consts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.277 +    @{command_def "thm_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.278 +    @{command_def "unused_thms"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.279 +    @{command_def "print_facts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.280 +    @{command_def "print_term_bindings"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.281    \end{matharray}
   1.282  
   1.283    @{rail \<open>
   1.284 @@ -495,73 +491,72 @@
   1.285    of rules declared for simplifications.
   1.286  
   1.287    \<^descr> @{command "print_theory"} prints the main logical content of the
   1.288 -  background theory; the ``@{text "!"}'' option indicates extra verbosity.
   1.289 +  background theory; the ``\<open>!\<close>'' option indicates extra verbosity.
   1.290  
   1.291    \<^descr> @{command "print_definitions"} prints dependencies of definitional
   1.292    specifications within the background theory, which may be constants
   1.293    \secref{sec:consts} or types (\secref{sec:types-pure},
   1.294 -  \secref{sec:hol-typedef}); the ``@{text "!"}'' option indicates extra
   1.295 +  \secref{sec:hol-typedef}); the ``\<open>!\<close>'' option indicates extra
   1.296    verbosity.
   1.297  
   1.298    \<^descr> @{command "print_methods"} prints all proof methods available in the
   1.299 -  current theory context; the ``@{text "!"}'' option indicates extra
   1.300 +  current theory context; the ``\<open>!\<close>'' option indicates extra
   1.301    verbosity.
   1.302  
   1.303    \<^descr> @{command "print_attributes"} prints all attributes available in the
   1.304 -  current theory context; the ``@{text "!"}'' option indicates extra
   1.305 +  current theory context; the ``\<open>!\<close>'' option indicates extra
   1.306    verbosity.
   1.307  
   1.308    \<^descr> @{command "print_theorems"} prints theorems of the background theory
   1.309 -  resulting from the last command; the ``@{text "!"}'' option indicates
   1.310 +  resulting from the last command; the ``\<open>!\<close>'' option indicates
   1.311    extra verbosity.
   1.312  
   1.313    \<^descr> @{command "print_facts"} prints all local facts of the current
   1.314 -  context, both named and unnamed ones; the ``@{text "!"}'' option indicates
   1.315 +  context, both named and unnamed ones; the ``\<open>!\<close>'' option indicates
   1.316    extra verbosity.
   1.317  
   1.318    \<^descr> @{command "print_term_bindings"} prints all term bindings that
   1.319    are present in the context.
   1.320  
   1.321 -  \<^descr> @{command "find_theorems"}~@{text criteria} retrieves facts
   1.322 +  \<^descr> @{command "find_theorems"}~\<open>criteria\<close> retrieves facts
   1.323    from the theory or proof context matching all of given search
   1.324 -  criteria.  The criterion @{text "name: p"} selects all theorems
   1.325 -  whose fully qualified name matches pattern @{text p}, which may
   1.326 -  contain ``@{text "*"}'' wildcards.  The criteria @{text intro},
   1.327 -  @{text elim}, and @{text dest} select theorems that match the
   1.328 +  criteria.  The criterion \<open>name: p\<close> selects all theorems
   1.329 +  whose fully qualified name matches pattern \<open>p\<close>, which may
   1.330 +  contain ``\<open>*\<close>'' wildcards.  The criteria \<open>intro\<close>,
   1.331 +  \<open>elim\<close>, and \<open>dest\<close> select theorems that match the
   1.332    current goal as introduction, elimination or destruction rules,
   1.333 -  respectively.  The criterion @{text "solves"} returns all rules
   1.334 +  respectively.  The criterion \<open>solves\<close> returns all rules
   1.335    that would directly solve the current goal.  The criterion
   1.336 -  @{text "simp: t"} selects all rewrite rules whose left-hand side
   1.337 -  matches the given term.  The criterion term @{text t} selects all
   1.338 -  theorems that contain the pattern @{text t} -- as usual, patterns
   1.339 -  may contain occurrences of the dummy ``@{text _}'', schematic
   1.340 +  \<open>simp: t\<close> selects all rewrite rules whose left-hand side
   1.341 +  matches the given term.  The criterion term \<open>t\<close> selects all
   1.342 +  theorems that contain the pattern \<open>t\<close> -- as usual, patterns
   1.343 +  may contain occurrences of the dummy ``\<open>_\<close>'', schematic
   1.344    variables, and type constraints.
   1.345  
   1.346 -  Criteria can be preceded by ``@{text "-"}'' to select theorems that
   1.347 +  Criteria can be preceded by ``\<open>-\<close>'' to select theorems that
   1.348    do \<^emph>\<open>not\<close> match. Note that giving the empty list of criteria
   1.349    yields \<^emph>\<open>all\<close> currently known facts.  An optional limit for the
   1.350    number of printed facts may be given; the default is 40.  By
   1.351    default, duplicates are removed from the search result. Use
   1.352 -  @{text with_dups} to display duplicates.
   1.353 +  \<open>with_dups\<close> to display duplicates.
   1.354  
   1.355 -  \<^descr> @{command "find_consts"}~@{text criteria} prints all constants
   1.356 -  whose type meets all of the given criteria. The criterion @{text
   1.357 -  "strict: ty"} is met by any type that matches the type pattern
   1.358 -  @{text ty}.  Patterns may contain both the dummy type ``@{text _}''
   1.359 -  and sort constraints. The criterion @{text ty} is similar, but it
   1.360 -  also matches against subtypes. The criterion @{text "name: p"} and
   1.361 -  the prefix ``@{text "-"}'' function as described for @{command
   1.362 +  \<^descr> @{command "find_consts"}~\<open>criteria\<close> prints all constants
   1.363 +  whose type meets all of the given criteria. The criterion \<open>strict: ty\<close> is met by any type that matches the type pattern
   1.364 +  \<open>ty\<close>.  Patterns may contain both the dummy type ``\<open>_\<close>''
   1.365 +  and sort constraints. The criterion \<open>ty\<close> is similar, but it
   1.366 +  also matches against subtypes. The criterion \<open>name: p\<close> and
   1.367 +  the prefix ``\<open>-\<close>'' function as described for @{command
   1.368    "find_theorems"}.
   1.369  
   1.370 -  \<^descr> @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
   1.371 +  \<^descr> @{command "thm_deps"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>
   1.372    visualizes dependencies of facts, using Isabelle's graph browser
   1.373    tool (see also @{cite "isabelle-system"}).
   1.374  
   1.375 -  \<^descr> @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"}
   1.376 -  displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}
   1.377 -  or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and
   1.378 +  \<^descr> @{command "unused_thms"}~\<open>A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n\<close>
   1.379 +  displays all theorems that are proved in theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close>
   1.380 +  or their parents but not in \<open>A\<^sub>1 \<dots> A\<^sub>m\<close> or their parents and
   1.381    that are never used.
   1.382 -  If @{text n} is @{text 0}, the end of the range of theories
   1.383 +  If \<open>n\<close> is \<open>0\<close>, the end of the range of theories
   1.384    defaults to the current theory. If no range is specified,
   1.385    only the unused theorems in the current theory are displayed.
   1.386  \<close>