added logic-specific sessions;
authorwenzelm
Wed May 07 12:38:55 2008 +0200 (2008-05-07)
changeset 26840ec46381f149d
parent 26839 1d963bfd4a1b
child 26841 6ac51a2f48e1
added logic-specific sessions;
doc-src/IsarRef/IsaMakefile
doc-src/IsarRef/Thy/HOLCF_Specific.thy
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/ROOT-HOLCF.ML
doc-src/IsarRef/Thy/ROOT-ZF.ML
doc-src/IsarRef/Thy/ROOT.ML
doc-src/IsarRef/Thy/ZF_Specific.thy
doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
doc-src/IsarRef/Thy/document/HOL_Specific.tex
doc-src/IsarRef/Thy/document/ZF_Specific.tex
doc-src/IsarRef/Thy/document/session.tex
doc-src/IsarRef/isar-ref.tex
     1.1 --- a/doc-src/IsarRef/IsaMakefile	Wed May 07 10:59:54 2008 +0200
     1.2 +++ b/doc-src/IsarRef/IsaMakefile	Wed May 07 12:38:55 2008 +0200
     1.3 @@ -1,9 +1,9 @@
     1.4  
     1.5  ## targets
     1.6  
     1.7 -default: Thy
     1.8 +default: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
     1.9  images: 
    1.10 -test: Thy
    1.11 +test: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
    1.12  
    1.13  all: images test
    1.14  
    1.15 @@ -17,16 +17,28 @@
    1.16  USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
    1.17  
    1.18  
    1.19 -## Thy
    1.20 +## IsarRef sessions
    1.21 +
    1.22 +HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
    1.23  
    1.24 -Thy: $(LOG)/HOL-Thy.gz
    1.25 +$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
    1.26 +  Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/Quick_Reference.thy
    1.27 +	@$(USEDIR) -s IsarRef HOL Thy
    1.28 +
    1.29  
    1.30 -$(LOG)/HOL-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
    1.31 -  Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/Quick_Reference.thy
    1.32 -	@$(USEDIR) HOL Thy
    1.33 +HOLCF-IsarRef: $(LOG)/HOLCF-IsarRef.gz
    1.34 +
    1.35 +$(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML Thy/HOLCF_Specific.thy
    1.36 +	@$(USEDIR) -s IsarRef -f ROOT-HOLCF.ML HOLCF Thy
    1.37 +
    1.38 +
    1.39 +ZF-IsarRef: $(LOG)/ZF-IsarRef.gz
    1.40 +
    1.41 +$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML Thy/ZF_Specific.thy
    1.42 +	@$(USEDIR) -s IsarRef -f ROOT-ZF.ML ZF Thy
    1.43  
    1.44  
    1.45  ## clean
    1.46  
    1.47  clean:
    1.48 -	@rm -f $(LOG)/HOL-Thy.gz
    1.49 +	@rm -f $(LOG)/HOL-IsarRef.gz $(LOG)/HOLCF-IsarRef.gz $(LOG)/ZF-IsarRef.gz
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Wed May 07 12:38:55 2008 +0200
     2.3 @@ -0,0 +1,7 @@
     2.4 +(* $Id$ *)
     2.5 +
     2.6 +theory HOLCF_Specific
     2.7 +imports HOLCF
     2.8 +begin
     2.9 +
    2.10 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed May 07 12:38:55 2008 +0200
     3.3 @@ -0,0 +1,7 @@
     3.4 +(* $Id$ *)
     3.5 +
     3.6 +theory HOL_Specific
     3.7 +imports HOL
     3.8 +begin
     3.9 +
    3.10 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Wed May 07 12:38:55 2008 +0200
     4.3 @@ -0,0 +1,5 @@
     4.4 +
     4.5 +(* $Id$ *)
     4.6 +
     4.7 +use "../../antiquote_setup.ML";
     4.8 +use_thy "HOLCF_Specific";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML	Wed May 07 12:38:55 2008 +0200
     5.3 @@ -0,0 +1,5 @@
     5.4 +
     5.5 +(* $Id$ *)
     5.6 +
     5.7 +use "../../antiquote_setup.ML";
     5.8 +use_thy "ZF_Specific";
     6.1 --- a/doc-src/IsarRef/Thy/ROOT.ML	Wed May 07 10:59:54 2008 +0200
     6.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML	Wed May 07 12:38:55 2008 +0200
     6.3 @@ -6,4 +6,5 @@
     6.4  use_thy "syntax";
     6.5  use_thy "pure";
     6.6  use_thy "Generic";
     6.7 +use_thy "HOL_Specific";
     6.8  use_thy "Quick_Reference";
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Wed May 07 12:38:55 2008 +0200
     7.3 @@ -0,0 +1,7 @@
     7.4 +(* $Id$ *)
     7.5 +
     7.6 +theory ZF_Specific
     7.7 +imports ZF
     7.8 +begin
     7.9 +
    7.10 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Wed May 07 12:38:55 2008 +0200
     8.3 @@ -0,0 +1,30 @@
     8.4 +%
     8.5 +\begin{isabellebody}%
     8.6 +\def\isabellecontext{HOLCF{\isacharunderscore}Specific}%
     8.7 +%
     8.8 +\isadelimtheory
     8.9 +\isanewline
    8.10 +\isanewline
    8.11 +%
    8.12 +\endisadelimtheory
    8.13 +%
    8.14 +\isatagtheory
    8.15 +\isacommand{theory}\isamarkupfalse%
    8.16 +\ HOLCF{\isacharunderscore}Specific\isanewline
    8.17 +\isakeyword{imports}\ HOLCF\isanewline
    8.18 +\isakeyword{begin}\isanewline
    8.19 +\isanewline
    8.20 +\isacommand{end}\isamarkupfalse%
    8.21 +%
    8.22 +\endisatagtheory
    8.23 +{\isafoldtheory}%
    8.24 +%
    8.25 +\isadelimtheory
    8.26 +\isanewline
    8.27 +%
    8.28 +\endisadelimtheory
    8.29 +\end{isabellebody}%
    8.30 +%%% Local Variables:
    8.31 +%%% mode: latex
    8.32 +%%% TeX-master: "root"
    8.33 +%%% End:
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed May 07 12:38:55 2008 +0200
     9.3 @@ -0,0 +1,30 @@
     9.4 +%
     9.5 +\begin{isabellebody}%
     9.6 +\def\isabellecontext{HOL{\isacharunderscore}Specific}%
     9.7 +%
     9.8 +\isadelimtheory
     9.9 +\isanewline
    9.10 +\isanewline
    9.11 +%
    9.12 +\endisadelimtheory
    9.13 +%
    9.14 +\isatagtheory
    9.15 +\isacommand{theory}\isamarkupfalse%
    9.16 +\ HOL{\isacharunderscore}Specific\isanewline
    9.17 +\isakeyword{imports}\ HOL\isanewline
    9.18 +\isakeyword{begin}\isanewline
    9.19 +\isanewline
    9.20 +\isacommand{end}\isamarkupfalse%
    9.21 +%
    9.22 +\endisatagtheory
    9.23 +{\isafoldtheory}%
    9.24 +%
    9.25 +\isadelimtheory
    9.26 +\isanewline
    9.27 +%
    9.28 +\endisadelimtheory
    9.29 +\end{isabellebody}%
    9.30 +%%% Local Variables:
    9.31 +%%% mode: latex
    9.32 +%%% TeX-master: "root"
    9.33 +%%% End:
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Wed May 07 12:38:55 2008 +0200
    10.3 @@ -0,0 +1,30 @@
    10.4 +%
    10.5 +\begin{isabellebody}%
    10.6 +\def\isabellecontext{ZF{\isacharunderscore}Specific}%
    10.7 +%
    10.8 +\isadelimtheory
    10.9 +\isanewline
   10.10 +\isanewline
   10.11 +%
   10.12 +\endisadelimtheory
   10.13 +%
   10.14 +\isatagtheory
   10.15 +\isacommand{theory}\isamarkupfalse%
   10.16 +\ ZF{\isacharunderscore}Specific\isanewline
   10.17 +\isakeyword{imports}\ ZF\isanewline
   10.18 +\isakeyword{begin}\isanewline
   10.19 +\isanewline
   10.20 +\isacommand{end}\isamarkupfalse%
   10.21 +%
   10.22 +\endisatagtheory
   10.23 +{\isafoldtheory}%
   10.24 +%
   10.25 +\isadelimtheory
   10.26 +\isanewline
   10.27 +%
   10.28 +\endisadelimtheory
   10.29 +\end{isabellebody}%
   10.30 +%%% Local Variables:
   10.31 +%%% mode: latex
   10.32 +%%% TeX-master: "root"
   10.33 +%%% End:
    11.1 --- a/doc-src/IsarRef/Thy/document/session.tex	Wed May 07 10:59:54 2008 +0200
    11.2 +++ b/doc-src/IsarRef/Thy/document/session.tex	Wed May 07 12:38:55 2008 +0200
    11.3 @@ -1,12 +1,4 @@
    11.4 -\input{intro.tex}
    11.5 -
    11.6 -\input{syntax.tex}
    11.7 -
    11.8 -\input{pure.tex}
    11.9 -
   11.10 -\input{Generic.tex}
   11.11 -
   11.12 -\input{Quick_Reference.tex}
   11.13 +\input{ZF_Specific.tex}
   11.14  
   11.15  %%% Local Variables:
   11.16  %%% mode: latex
    12.1 --- a/doc-src/IsarRef/isar-ref.tex	Wed May 07 10:59:54 2008 +0200
    12.2 +++ b/doc-src/IsarRef/isar-ref.tex	Wed May 07 12:38:55 2008 +0200
    12.3 @@ -79,6 +79,9 @@
    12.4  \input{Thy/document/syntax.tex}
    12.5  \input{Thy/document/pure.tex}
    12.6  \input{Thy/document/Generic.tex}
    12.7 +\input{Thy/document/HOL_Specific.tex}
    12.8 +\input{Thy/document/HOLCF_Specific.tex}
    12.9 +\input{Thy/document/ZF_Specific.tex}
   12.10  \input{logics.tex}
   12.11  
   12.12  \appendix