--- a/doc-src/IsarRef/IsaMakefile Fri May 09 23:21:33 2008 +0200
+++ b/doc-src/IsarRef/IsaMakefile Fri May 09 23:35:57 2008 +0200
@@ -22,8 +22,8 @@
HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
- Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/HOL_Specific.thy \
- Thy/Quick_Reference.thy Thy/ML_Tactic.thy
+ Thy/syntax.thy Thy/Spec.thy Thy/Proof.thy Thy/pure.thy Thy/Generic.thy \
+ Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/ML_Tactic.thy
@$(USEDIR) -s IsarRef HOL Thy
--- a/doc-src/IsarRef/Makefile Fri May 09 23:21:33 2008 +0200
+++ b/doc-src/IsarRef/Makefile Fri May 09 23:35:57 2008 +0200
@@ -15,7 +15,8 @@
FILES = isar-ref.tex style.sty basics.tex Thy/document/Generic.tex \
Thy/document/HOLCF_Specific.tex Thy/document/HOL_Specific.tex \
- Thy/document/ML_Tactic.tex Thy/document/Quick_Reference.tex \
+ Thy/document/ML_Tactic.tex Thy/document/Proof.tex \
+ Thy/document/Quick_Reference.tex Thy/document/Spec.tex \
Thy/document/ZF_Specific.tex Thy/document/intro.tex \
Thy/document/pure.tex Thy/document/syntax.tex \
../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/Proof.thy Fri May 09 23:35:57 2008 +0200
@@ -0,0 +1,9 @@
+(* $Id$ *)
+
+theory Proof
+imports Main
+begin
+
+chapter {* Proofs *}
+
+end
--- a/doc-src/IsarRef/Thy/ROOT.ML Fri May 09 23:21:33 2008 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML Fri May 09 23:35:57 2008 +0200
@@ -6,6 +6,8 @@
use_thy "intro";
use_thy "syntax";
+use_thy "Spec";
+use_thy "Proof";
use_thy "pure";
use_thy "Generic";
use_thy "HOL_Specific";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/Spec.thy Fri May 09 23:35:57 2008 +0200
@@ -0,0 +1,9 @@
+(* $Id$ *)
+
+theory Spec
+imports Main
+begin
+
+chapter {* Specifications *}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Fri May 09 23:35:57 2008 +0200
@@ -0,0 +1,45 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Proof}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Proof\isanewline
+\isakeyword{imports}\ Main\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Proofs%
+}
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Fri May 09 23:35:57 2008 +0200
@@ -0,0 +1,45 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Spec}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Spec\isanewline
+\isakeyword{imports}\ Main\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Specifications%
+}
+\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/IsarRef/isar-ref.tex Fri May 09 23:21:33 2008 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Fri May 09 23:35:57 2008 +0200
@@ -65,6 +65,8 @@
\input{Thy/document/intro.tex}
\input{basics.tex}
\input{Thy/document/syntax.tex}
+\input{Thy/document/Spec.tex}
+\input{Thy/document/Proof.tex}
\input{Thy/document/pure.tex}
\input{Thy/document/Generic.tex}
\input{Thy/document/HOL_Specific.tex}