# HG changeset patch
# User wenzelm
# Date 1210156735 -7200
# Node ID ec46381f149df17e5161eb80b72e9895fe0649ba
# Parent  1d963bfd4a1bbd0a6301687b722ba56db90fd62d
added logic-specific sessions;

diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/IsaMakefile
--- 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
diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/Thy/HOLCF_Specific.thy
--- /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
diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/Thy/HOL_Specific.thy
--- /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
diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/Thy/ROOT-HOLCF.ML
--- /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";
diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/Thy/ROOT-ZF.ML
--- /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";
diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/Thy/ROOT.ML
--- 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";
diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/Thy/ZF_Specific.thy
--- /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
diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
--- /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:
diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- /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:
diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/Thy/document/ZF_Specific.tex
--- /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:
diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/Thy/document/session.tex
--- 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
diff -r 1d963bfd4a1b -r ec46381f149d doc-src/IsarRef/isar-ref.tex
--- 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