--- a/doc-src/IsarImplementation/IsaMakefile Thu Feb 26 20:57:59 2009 +0100
+++ b/doc-src/IsarImplementation/IsaMakefile Thu Feb 26 21:16:53 2009 +0100
@@ -23,7 +23,8 @@
$(LOG)/Pure-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Integration.thy \
Thy/Isar.thy Thy/Local_Theory.thy Thy/Logic.thy Thy/Prelim.thy \
- Thy/Proof.thy Thy/Tactic.thy Thy/ML.thy ../antiquote_setup.ML
+ Thy/Proof.thy Thy/Syntax.thy Thy/Tactic.thy Thy/ML.thy \
+ ../antiquote_setup.ML
@$(USEDIR) Pure Thy
--- a/doc-src/IsarImplementation/Makefile Thu Feb 26 20:57:59 2009 +0100
+++ b/doc-src/IsarImplementation/Makefile Thu Feb 26 21:16:53 2009 +0100
@@ -10,12 +10,12 @@
NAME = implementation
-FILES = implementation.tex Thy/document/Prelim.tex \
- Thy/document/Logic.tex Thy/document/Tactic.tex \
- Thy/document/Proof.tex Thy/document/Local_Theory.tex \
- Thy/document/Integration.tex style.sty ../iman.sty ../extra.sty \
- ../isar.sty ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \
- ../manual.bib ../proof.sty
+FILES = ../extra.sty ../iman.sty ../isabelle.sty ../isabellesym.sty \
+ ../isar.sty ../manual.bib ../pdfsetup.sty ../proof.sty \
+ Thy/document/Integration.tex Thy/document/Local_Theory.tex \
+ Thy/document/Logic.tex Thy/document/Prelim.tex \
+ Thy/document/Proof.tex Thy/document/Syntax.tex \
+ Thy/document/Tactic.tex implementation.tex style.sty
dvi: $(NAME).dvi
--- a/doc-src/IsarImplementation/Thy/ROOT.ML Thu Feb 26 20:57:59 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/ROOT.ML Thu Feb 26 21:16:53 2009 +0100
@@ -1,8 +1,11 @@
-use_thy "Prelim";
-use_thy "Logic";
-use_thy "Tactic";
-use_thy "Proof";
-use_thy "Isar";
-use_thy "Local_Theory";
-use_thy "Integration";
-use_thy "ML";
+use_thys [
+ "Integration",
+ "Isar",
+ "Local_Theory",
+ "Logic",
+ "ML",
+ "Prelim",
+ "Proof",
+ "Syntax",
+ "Tactic"
+];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy Thu Feb 26 21:16:53 2009 +0100
@@ -0,0 +1,9 @@
+theory Syntax
+imports Base
+begin
+
+chapter {* Syntax and type-checking *}
+
+text FIXME
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex Thu Feb 26 21:16:53 2009 +0100
@@ -0,0 +1,48 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Syntax}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Syntax\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Syntax and type-checking%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/IsarImplementation/Thy/document/session.tex Thu Feb 26 20:57:59 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/session.tex Thu Feb 26 21:16:53 2009 +0100
@@ -1,21 +1,23 @@
\input{Base.tex}
-\input{Prelim.tex}
-
-\input{Logic.tex}
-
-\input{Tactic.tex}
-
-\input{Proof.tex}
+\input{Integration.tex}
\input{Isar.tex}
\input{Local_Theory.tex}
-\input{Integration.tex}
+\input{Logic.tex}
\input{ML.tex}
+\input{Prelim.tex}
+
+\input{Proof.tex}
+
+\input{Syntax.tex}
+
+\input{Tactic.tex}
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/IsarImplementation/implementation.tex Thu Feb 26 20:57:59 2009 +0100
+++ b/doc-src/IsarImplementation/implementation.tex Thu Feb 26 21:16:53 2009 +0100
@@ -69,6 +69,7 @@
\input{Thy/document/Logic.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}