# 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