# HG changeset patch
# User wenzelm
# Date 1235679413 -3600
# Node ID b956bf0dc87c6f4973338db473fe5614de2cd149
# Parent  25a3531c0df5aa19ed57f377faf36332e64614c9
basic setup for chapter "Syntax and type-checking";

diff -r 25a3531c0df5 -r b956bf0dc87c doc-src/IsarImplementation/IsaMakefile
--- 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
 
 
diff -r 25a3531c0df5 -r b956bf0dc87c doc-src/IsarImplementation/Makefile
--- 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
 
diff -r 25a3531c0df5 -r b956bf0dc87c doc-src/IsarImplementation/Thy/ROOT.ML
--- 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"
+];
diff -r 25a3531c0df5 -r b956bf0dc87c doc-src/IsarImplementation/Thy/Syntax.thy
--- /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
diff -r 25a3531c0df5 -r b956bf0dc87c doc-src/IsarImplementation/Thy/document/Syntax.tex
--- /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:
diff -r 25a3531c0df5 -r b956bf0dc87c doc-src/IsarImplementation/Thy/document/session.tex
--- 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"
diff -r 25a3531c0df5 -r b956bf0dc87c doc-src/IsarImplementation/implementation.tex
--- 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}