--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Oct 12 18:18:48 2015 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Oct 12 19:32:25 2015 +0200
@@ -1036,12 +1036,11 @@
text \<open>The ML datatype @{ML_type Ast.ast} explicitly represents the
intermediate AST format that is used for syntax rewriting
(\secref{sec:syn-trans}). It is defined in ML as follows:
- \begin{ttbox}
- datatype ast =
- Constant of string |
- Variable of string |
- Appl of ast list
- \end{ttbox}
+ @{verbatim [display]
+\<open>datatype ast =
+ Constant of string |
+ Variable of string |
+ Appl of ast list\<close>}
An AST is either an atom (constant or variable) or a list of (at
least two) subtrees. Occasional diagnostic output of ASTs uses
--- a/src/Doc/Isar_Ref/Proof.thy Mon Oct 12 18:18:48 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Mon Oct 12 19:32:25 2015 +0200
@@ -484,11 +484,7 @@
of @{command "show"} predicts potential failure and displays the
resulting error as a warning beforehand. Watch out for the
following message:
-
- %FIXME proper antiquotation
- \begin{ttbox}
- Problem! Local statement will fail to solve any pending goal
- \end{ttbox}
+ @{verbatim [display] \<open>Local statement fails to refine any pending goal\<close>}
\item @{command "hence"} abbreviates ``@{command "then"}~@{command
"have"}'', i.e.\ claims a local goal to be proven by forward
--- a/src/Doc/JEdit/JEdit.thy Mon Oct 12 18:18:48 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy Mon Oct 12 19:32:25 2015 +0200
@@ -222,8 +222,8 @@
Nonetheless it is occasionally useful to invoke the Prover IDE on the
command-line, with some extra options and environment settings as explained
below. The command-line usage of @{tool_def jedit} is as follows:
-\begin{ttbox}
- Usage: isabelle jedit [OPTIONS] [FILES ...]
+ @{verbatim [display]
+\<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
Options are:
-J OPTION add JVM runtime option
@@ -237,8 +237,7 @@
-s system build mode for session image
Start jEdit with Isabelle plugin setup and open theory FILES
- (default "\$USER_HOME/Scratch.thy").
-\end{ttbox}
+ (default "$USER_HOME/Scratch.thy").\<close>}
The @{verbatim "-l"} option specifies the session name of the logic
image to be used for proof processing. Additional session root
--- a/src/Doc/JEdit/document/root.tex Mon Oct 12 18:18:48 2015 +0200
+++ b/src/Doc/JEdit/document/root.tex Mon Oct 12 19:32:25 2015 +0200
@@ -18,6 +18,7 @@
\isadroptag{theory}
\isabellestyle{literal}
+\def\isastylett{\footnotesize\tt}
\title{\includegraphics[scale=0.5]{isabelle_jedit} \\[4ex] Isabelle/jEdit}