# HG changeset patch
# User wenzelm
# Date 1287170576 -3600
# Node ID 9c977f899ebfba357b7f2605011ecf1b4fa060e7
# Parent  7219a771ab63a3338d639f3715de4751f2fe07a8
tuned chapter arrangement;

diff -r 7219a771ab63 -r 9c977f899ebf doc-src/IsarImplementation/Thy/Syntax.thy
--- a/doc-src/IsarImplementation/Thy/Syntax.thy	Fri Oct 15 19:54:34 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy	Fri Oct 15 20:22:56 2010 +0100
@@ -6,10 +6,14 @@
 
 text FIXME
 
+
 section {* Parsing and printing *}
 
 text FIXME
 
+
 section {* Checking and unchecking \label{sec:term-check} *}
 
+text FIXME
+
 end
diff -r 7219a771ab63 -r 9c977f899ebf doc-src/IsarImplementation/Thy/Tactic.thy
--- a/doc-src/IsarImplementation/Thy/Tactic.thy	Fri Oct 15 19:54:34 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy	Fri Oct 15 20:22:56 2010 +0100
@@ -406,6 +406,8 @@
   Various search strategies may be expressed via tacticals.
 
   \medskip FIXME
-*}
+
+  \medskip The chapter on tacticals in \cite{isabelle-ref} is still
+  applicable, despite a few outdated details.  *}
 
 end
diff -r 7219a771ab63 -r 9c977f899ebf doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Fri Oct 15 19:54:34 2010 +0100
+++ b/doc-src/IsarImplementation/implementation.tex	Fri Oct 15 20:22:56 2010 +0100
@@ -87,9 +87,9 @@
 \input{Thy/document/ML.tex}
 \input{Thy/document/Prelim.tex}
 \input{Thy/document/Logic.tex}
+\input{Thy/document/Syntax.tex}
 \input{Thy/document/Tactic.tex}
 \input{Thy/document/Proof.tex}
-\input{Thy/document/Syntax.tex}
 \input{Thy/document/Isar.tex}
 \input{Thy/document/Local_Theory.tex}
 \input{Thy/document/Integration.tex}
diff -r 7219a771ab63 -r 9c977f899ebf doc-src/manual.bib
--- a/doc-src/manual.bib	Fri Oct 15 19:54:34 2010 +0100
+++ b/doc-src/manual.bib	Fri Oct 15 20:22:56 2010 +0100
@@ -1053,7 +1053,7 @@
 
 @manual{isabelle-intro,
   author	= {Lawrence C. Paulson},
-  title		= {Introduction to {Isabelle}},
+  title		= {Old Introduction to {Isabelle}},
   institution	= CUCL,
   note          = {\url{http://isabelle.in.tum.de/doc/intro.pdf}}}
 
@@ -1065,7 +1065,7 @@
 
 @manual{isabelle-ref,
   author	= {Lawrence C. Paulson},
-  title		= {The {Isabelle} Reference Manual},
+  title		= {The Old {Isabelle} Reference Manual},
   institution	= CUCL,
   note          = {\url{http://isabelle.in.tum.de/doc/ref.pdf}}}