--- a/src/Doc/IsarImplementation/Eq.thy Sun Sep 29 12:44:40 2013 +0200
+++ b/src/Doc/IsarImplementation/Eq.thy Sun Sep 29 12:49:47 2013 +0200
@@ -63,7 +63,7 @@
@{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
\end{mldecls}
- See also @{"file" "~~/src/Pure/thm.ML" } for further description of
+ See also @{file "~~/src/Pure/thm.ML" } for further description of
these inference rules, and a few more for primitive @{text "\<beta>"} and
@{text "\<eta>"} conversions. Note that @{text "\<alpha>"} conversion is
implicit due to the representation of terms with de-Bruijn indices
--- a/src/Doc/IsarImplementation/ML.thy Sun Sep 29 12:44:40 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy Sun Sep 29 12:49:47 2013 +0200
@@ -2086,7 +2086,7 @@
text {*
%FIXME
- See also @{"file" "~~/src/Pure/Concurrent/lazy.ML"}.
+ See also @{file "~~/src/Pure/Concurrent/lazy.ML"}.
*}
@@ -2095,7 +2095,7 @@
text {*
%FIXME
- See also @{"file" "~~/src/Pure/Concurrent/future.ML"}.
+ See also @{file "~~/src/Pure/Concurrent/future.ML"}.
*}
--- a/src/Doc/IsarRef/Document_Preparation.thy Sun Sep 29 12:44:40 2013 +0200
+++ b/src/Doc/IsarRef/Document_Preparation.thy Sun Sep 29 12:49:47 2013 +0200
@@ -451,7 +451,7 @@
The @{antiquotation rail} antiquotation allows to include syntax
diagrams into Isabelle documents. {\LaTeX} requires the style file
- @{"file" "~~/lib/texinputs/pdfsetup.sty"}, which can be used via
+ @{file "~~/lib/texinputs/pdfsetup.sty"}, which can be used via
@{verbatim "\\usepackage{pdfsetup}"} in @{verbatim "root.tex"}, for
example.
--- a/src/Doc/IsarRef/HOL_Specific.thy Sun Sep 29 12:44:40 2013 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy Sun Sep 29 12:49:47 2013 +0200
@@ -1887,7 +1887,7 @@
using assms by (algebra add: collinear.simps)
text {*
- See also @{"file" "~~/src/HOL/ex/Groebner_Examples.thy"}.
+ See also @{file "~~/src/HOL/ex/Groebner_Examples.thy"}.
*}
--- a/src/Doc/JEdit/JEdit.thy Sun Sep 29 12:44:40 2013 +0200
+++ b/src/Doc/JEdit/JEdit.thy Sun Sep 29 12:49:47 2013 +0200
@@ -104,7 +104,7 @@
\medskip
A default mapping relates some Isabelle symbols to Unicode points (see
- @{file "~~/etc/symbols"} and @{verbatim
+ @{file "$ISABELLE_HOME/etc/symbols"} and @{verbatim
"$ISABELLE_HOME_USER/etc/symbols"}.
The \emph{IsabelleText} font ensures that Unicode points are actually seen
@@ -191,8 +191,9 @@
Isabelle Symbols are completed in backslashed forms, e.g. @{verbatim
"\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
- symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
- abbreviations may be used as specified in @{file "~~/etc/symbols"}.
+ symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
+ abbreviations may be used as specified in @{file
+ "$ISABELLE_HOME/etc/symbols"}.
\emph{Explicit completion} works via standard jEdit shortcut @{verbatim
"C+b"}, which is remapped to action @{verbatim "isabelle.complete"}, with a
--- a/src/Doc/System/Scala.thy Sun Sep 29 12:44:40 2013 +0200
+++ b/src/Doc/System/Scala.thy Sun Sep 29 12:49:47 2013 +0200
@@ -90,7 +90,7 @@
Console.println("document = " + options.string("document"))
\end{alltt}
- Alternatively the full @{"file"
+ Alternatively the full @{file
"$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in
expanded form. *}