--- a/doc-src/IsarRef/IsaMakefile Wed May 07 10:59:54 2008 +0200
+++ b/doc-src/IsarRef/IsaMakefile Wed May 07 12:38:55 2008 +0200
@@ -1,9 +1,9 @@
## targets
-default: Thy
+default: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
images:
-test: Thy
+test: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
all: images test
@@ -17,16 +17,28 @@
USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
-## Thy
+## IsarRef sessions
+
+HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
-Thy: $(LOG)/HOL-Thy.gz
+$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
+ Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/Quick_Reference.thy
+ @$(USEDIR) -s IsarRef HOL Thy
+
-$(LOG)/HOL-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
- Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/Quick_Reference.thy
- @$(USEDIR) HOL Thy
+HOLCF-IsarRef: $(LOG)/HOLCF-IsarRef.gz
+
+$(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML Thy/HOLCF_Specific.thy
+ @$(USEDIR) -s IsarRef -f ROOT-HOLCF.ML HOLCF Thy
+
+
+ZF-IsarRef: $(LOG)/ZF-IsarRef.gz
+
+$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML Thy/ZF_Specific.thy
+ @$(USEDIR) -s IsarRef -f ROOT-ZF.ML ZF Thy
## clean
clean:
- @rm -f $(LOG)/HOL-Thy.gz
+ @rm -f $(LOG)/HOL-IsarRef.gz $(LOG)/HOLCF-IsarRef.gz $(LOG)/ZF-IsarRef.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy Wed May 07 12:38:55 2008 +0200
@@ -0,0 +1,7 @@
+(* $Id$ *)
+
+theory HOLCF_Specific
+imports HOLCF
+begin
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 07 12:38:55 2008 +0200
@@ -0,0 +1,7 @@
+(* $Id$ *)
+
+theory HOL_Specific
+imports HOL
+begin
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML Wed May 07 12:38:55 2008 +0200
@@ -0,0 +1,5 @@
+
+(* $Id$ *)
+
+use "../../antiquote_setup.ML";
+use_thy "HOLCF_Specific";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML Wed May 07 12:38:55 2008 +0200
@@ -0,0 +1,5 @@
+
+(* $Id$ *)
+
+use "../../antiquote_setup.ML";
+use_thy "ZF_Specific";
--- a/doc-src/IsarRef/Thy/ROOT.ML Wed May 07 10:59:54 2008 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML Wed May 07 12:38:55 2008 +0200
@@ -6,4 +6,5 @@
use_thy "syntax";
use_thy "pure";
use_thy "Generic";
+use_thy "HOL_Specific";
use_thy "Quick_Reference";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/ZF_Specific.thy Wed May 07 12:38:55 2008 +0200
@@ -0,0 +1,7 @@
+(* $Id$ *)
+
+theory ZF_Specific
+imports ZF
+begin
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Wed May 07 12:38:55 2008 +0200
@@ -0,0 +1,30 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{HOLCF{\isacharunderscore}Specific}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ HOLCF{\isacharunderscore}Specific\isanewline
+\isakeyword{imports}\ HOLCF\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+\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/HOL_Specific.tex Wed May 07 12:38:55 2008 +0200
@@ -0,0 +1,30 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{HOL{\isacharunderscore}Specific}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ HOL{\isacharunderscore}Specific\isanewline
+\isakeyword{imports}\ HOL\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+\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/ZF_Specific.tex Wed May 07 12:38:55 2008 +0200
@@ -0,0 +1,30 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{ZF{\isacharunderscore}Specific}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ ZF{\isacharunderscore}Specific\isanewline
+\isakeyword{imports}\ ZF\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/IsarRef/Thy/document/session.tex Wed May 07 10:59:54 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/session.tex Wed May 07 12:38:55 2008 +0200
@@ -1,12 +1,4 @@
-\input{intro.tex}
-
-\input{syntax.tex}
-
-\input{pure.tex}
-
-\input{Generic.tex}
-
-\input{Quick_Reference.tex}
+\input{ZF_Specific.tex}
%%% Local Variables:
%%% mode: latex
--- a/doc-src/IsarRef/isar-ref.tex Wed May 07 10:59:54 2008 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Wed May 07 12:38:55 2008 +0200
@@ -79,6 +79,9 @@
\input{Thy/document/syntax.tex}
\input{Thy/document/pure.tex}
\input{Thy/document/Generic.tex}
+\input{Thy/document/HOL_Specific.tex}
+\input{Thy/document/HOLCF_Specific.tex}
+\input{Thy/document/ZF_Specific.tex}
\input{logics.tex}
\appendix