--- 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
--- 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
--- 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}
--- 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}}}