# HG changeset patch
# User wenzelm
# Date 1380451787 -7200
# Node ID f0ee922852219c70a23a454af9b39c7d9033cce7
# Parent  1f4d6870b7b22ddb43284fa65cb5edee4cc2a7f7
tuned;

diff -r 1f4d6870b7b2 -r f0ee92285221 src/Doc/IsarImplementation/Eq.thy
--- 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
diff -r 1f4d6870b7b2 -r f0ee92285221 src/Doc/IsarImplementation/ML.thy
--- 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"}.
 *}
 
 
diff -r 1f4d6870b7b2 -r f0ee92285221 src/Doc/IsarRef/Document_Preparation.thy
--- 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.
 
diff -r 1f4d6870b7b2 -r f0ee92285221 src/Doc/IsarRef/HOL_Specific.thy
--- 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"}.
 *}
 
 
diff -r 1f4d6870b7b2 -r f0ee92285221 src/Doc/JEdit/JEdit.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
diff -r 1f4d6870b7b2 -r f0ee92285221 src/Doc/System/Scala.thy
--- 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.  *}