# HG changeset patch
# User wenzelm
# Date 1210368957 -7200
# Node ID 3bc332135aa7cb6537ce0607ecee8e028041de75
# Parent  60058b050c58b444fa1c247bb6e6f9bec649c0e8
added chapters for "Specifications" and "Proofs";

diff -r 60058b050c58 -r 3bc332135aa7 doc-src/IsarRef/IsaMakefile
--- 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
 
 
diff -r 60058b050c58 -r 3bc332135aa7 doc-src/IsarRef/Makefile
--- 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 \
diff -r 60058b050c58 -r 3bc332135aa7 doc-src/IsarRef/Thy/Proof.thy
--- /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
diff -r 60058b050c58 -r 3bc332135aa7 doc-src/IsarRef/Thy/ROOT.ML
--- 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";
diff -r 60058b050c58 -r 3bc332135aa7 doc-src/IsarRef/Thy/Spec.thy
--- /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
diff -r 60058b050c58 -r 3bc332135aa7 doc-src/IsarRef/Thy/document/Proof.tex
--- /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:
diff -r 60058b050c58 -r 3bc332135aa7 doc-src/IsarRef/Thy/document/Spec.tex
--- /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:
diff -r 60058b050c58 -r 3bc332135aa7 doc-src/IsarRef/isar-ref.tex
--- 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}