1.1 --- a/doc-src/Classes/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,35 +0,0 @@
     1.4 -
     1.5 -## targets
     1.6 -
     1.7 -default: Thy
     1.8 -images: 
     1.9 -test: Thy
    1.10 -
    1.11 -all: images test
    1.12 -
    1.13 -
    1.14 -## global settings
    1.15 -
    1.16 -SRC = $(ISABELLE_HOME)/src
    1.17 -OUT = $(ISABELLE_OUTPUT)
    1.18 -LOG = $(OUT)/log
    1.19 -
    1.20 -USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
    1.21 -
    1.22 -
    1.23 -## Thy
    1.24 -
    1.25 -THY = $(LOG)/HOL-Thy.gz
    1.26 -
    1.27 -Thy: $(THY)
    1.28 -
    1.29 -$(THY): $(OUT)/HOL Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy ../antiquote_setup.ML ../more_antiquote.ML
    1.30 -	@$(USEDIR) HOL Thy
    1.31 -	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
    1.32 -	  Thy/document/pdfsetup.sty Thy/document/session.tex
    1.33 -
    1.34 -
    1.35 -## clean
    1.36 -
    1.37 -clean:
    1.38 -	@rm -f $(THY)

     2.1 --- a/doc-src/Classes/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,2 +0,0 @@
     2.4 -no_document use_thy "Setup";
     2.5 -use_thy "Classes";

     3.1 --- a/doc-src/Codegen/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,35 +0,0 @@
     3.4 -
     3.5 -## targets
     3.6 -
     3.7 -default: Thy
     3.8 -images: 
     3.9 -test: Thy
    3.10 -
    3.11 -all: images test
    3.12 -
    3.13 -
    3.14 -## global settings
    3.15 -
    3.16 -SRC = $(ISABELLE_HOME)/src
    3.17 -OUT = $(ISABELLE_OUTPUT)
    3.18 -LOG = $(OUT)/log
    3.19 -
    3.20 -USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
    3.21 -
    3.22 -
    3.23 -## Thy
    3.24 -
    3.25 -THY = $(LOG)/HOL-Thy.gz
    3.26 -
    3.27 -Thy: $(THY)
    3.28 -
    3.29 -$(THY): $(OUT)/HOL-Library Thy/ROOT.ML Thy/*.thy ../antiquote_setup.ML ../more_antiquote.ML
    3.30 -	@$(USEDIR) -m no_brackets -m iff HOL-Library Thy
    3.31 -	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
    3.32 -	  Thy/document/pdfsetup.sty Thy/document/session.tex
    3.33 -
    3.34 -
    3.35 -## clean
    3.36 -
    3.37 -clean:
    3.38 -	@rm -f $(THY)

     4.1 --- a/doc-src/Codegen/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,10 +0,0 @@
     4.4 -
     4.5 -no_document use_thy "Setup";
     4.6 -
     4.7 -use_thy "Introduction";
     4.8 -use_thy "Foundations";
     4.9 -use_thy "Refinement";
    4.10 -use_thy "Inductive_Predicate";
    4.11 -use_thy "Evaluation";
    4.12 -use_thy "Adaptation";
    4.13 -use_thy "Further";

     5.1 --- a/doc-src/Functions/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,35 +0,0 @@
     5.4 -
     5.5 -## targets
     5.6 -
     5.7 -default: Thy
     5.8 -images: 
     5.9 -test: Thy
    5.10 -
    5.11 -all: images test
    5.12 -
    5.13 -
    5.14 -## global settings
    5.15 -
    5.16 -SRC = $(ISABELLE_HOME)/src
    5.17 -OUT = $(ISABELLE_OUTPUT)
    5.18 -LOG = $(OUT)/log
    5.19 -
    5.20 -USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
    5.21 -
    5.22 -
    5.23 -## Thy
    5.24 -
    5.25 -THY = $(LOG)/HOL-Thy.gz
    5.26 -
    5.27 -Thy: $(THY)
    5.28 -
    5.29 -$(THY): $(OUT)/HOL Thy/ROOT.ML Thy/Functions.thy
    5.30 -	@$(USEDIR) HOL Thy
    5.31 -	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
    5.32 -	 Thy/document/pdfsetup.sty Thy/document/session.tex
    5.33 -
    5.34 -
    5.35 -## clean
    5.36 -
    5.37 -clean:
    5.38 -	@rm -f $(THY)

     6.1 --- a/doc-src/Functions/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,1 +0,0 @@
     6.4 -use_thy "Functions";

     7.1 --- a/doc-src/IsarImplementation/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,36 +0,0 @@
     7.4 -
     7.5 -## targets
     7.6 -
     7.7 -default: Thy
     7.8 -images: 
     7.9 -test: Thy
    7.10 -
    7.11 -all: images test
    7.12 -
    7.13 -
    7.14 -## global settings
    7.15 -
    7.16 -SRC = $(ISABELLE_HOME)/src
    7.17 -OUT = $(ISABELLE_OUTPUT)
    7.18 -LOG = $(OUT)/log
    7.19 -
    7.20 -USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
    7.21 -
    7.22 -
    7.23 -## sessions
    7.24 -
    7.25 -Thy: $(LOG)/HOL-Thy.gz
    7.26 -
    7.27 -$(LOG)/HOL-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Eq.thy			\
    7.28 -  Thy/Integration.thy Thy/Isar.thy Thy/Local_Theory.thy Thy/Logic.thy	\
    7.29 -  Thy/Prelim.thy Thy/Proof.thy Thy/Syntax.thy Thy/Tactic.thy		\
    7.30 -  Thy/ML.thy ../antiquote_setup.ML
    7.31 -	@$(USEDIR) HOL Thy
    7.32 -	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
    7.33 -	 Thy/document/pdfsetup.sty Thy/document/session.tex
    7.34 -
    7.35 -
    7.36 -## clean
    7.37 -
    7.38 -clean:
    7.39 -	@rm -f $(LOG)/HOL-Thy.gz

     8.1 --- a/doc-src/IsarImplementation/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,12 +0,0 @@
     8.4 -use_thys [
     8.5 -  "Eq",
     8.6 -  "Integration",
     8.7 -  "Isar",
     8.8 -  "Local_Theory",
     8.9 -  "Logic",
    8.10 -  "ML",
    8.11 -  "Prelim",
    8.12 -  "Proof",
    8.13 -  "Syntax",
    8.14 -  "Tactic"
    8.15 -];

     9.1 --- a/doc-src/IsarRef/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,56 +0,0 @@
     9.4 -
     9.5 -## targets
     9.6 -
     9.7 -default: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
     9.8 -images: 
     9.9 -test: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
    9.10 -
    9.11 -all: images test
    9.12 -
    9.13 -
    9.14 -## global settings
    9.15 -
    9.16 -SRC = $(ISABELLE_HOME)/src
    9.17 -OUT = $(ISABELLE_OUTPUT)
    9.18 -LOG = $(OUT)/log
    9.19 -
    9.20 -USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
    9.21 -
    9.22 -
    9.23 -## sessions
    9.24 -
    9.25 -HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
    9.26 -
    9.27 -$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/Base.thy	\
    9.28 -  Thy/First_Order_Logic.thy Thy/Framework.thy Thy/Inner_Syntax.thy	\
    9.29 -  Thy/Preface.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy	\
    9.30 -  Thy/Misc.thy Thy/Document_Preparation.thy Thy/Generic.thy		\
    9.31 -  Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/Synopsis.thy		\
    9.32 -  Thy/Symbols.thy Thy/ML_Tactic.thy
    9.33 -	@$(USEDIR) -s IsarRef HOL Thy
    9.34 -	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
    9.35 -	 Thy/document/pdfsetup.sty Thy/document/session.tex
    9.36 -
    9.37 -
    9.38 -HOLCF-IsarRef: $(LOG)/HOLCF-IsarRef.gz
    9.39 -
    9.40 -$(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML	\
    9.41 -  Thy/Base.thy Thy/HOLCF_Specific.thy
    9.42 -	@$(USEDIR) -s IsarRef -f ROOT-HOLCF.ML HOLCF Thy
    9.43 -	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
    9.44 -	 Thy/document/pdfsetup.sty Thy/document/session.tex
    9.45 -
    9.46 -
    9.47 -ZF-IsarRef: $(LOG)/ZF-IsarRef.gz
    9.48 -
    9.49 -$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML	\
    9.50 -  Thy/Base.thy Thy/ZF_Specific.thy
    9.51 -	@$(USEDIR) -s IsarRef -f ROOT-ZF.ML ZF Thy
    9.52 -	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
    9.53 -	 Thy/document/pdfsetup.sty Thy/document/session.tex
    9.54 -
    9.55 -
    9.56 -## clean
    9.57 -
    9.58 -clean:
    9.59 -	@rm -f $(LOG)/HOL-IsarRef.gz $(LOG)/HOLCF-IsarRef.gz $(LOG)/ZF-IsarRef.gz

    10.1 --- a/doc-src/IsarRef/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,19 +0,0 @@
    10.4 -quick_and_dirty := true;
    10.5 -
    10.6 -use_thys [
    10.7 -  "Preface",
    10.8 -  "Synopsis",
    10.9 -  "Framework",
   10.10 -  "First_Order_Logic",
   10.11 -  "Outer_Syntax",
   10.12 -  "Document_Preparation",
   10.13 -  "Spec",
   10.14 -  "Proof",
   10.15 -  "Inner_Syntax",
   10.16 -  "Misc",
   10.17 -  "Generic",
   10.18 -  "HOL_Specific",
   10.19 -  "Quick_Reference",
   10.20 -  "Symbols",
   10.21 -  "ML_Tactic"
   10.22 -];

    11.1 --- a/doc-src/LaTeXsugar/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,35 +0,0 @@
    11.4 -
    11.5 -## targets
    11.6 -
    11.7 -default: Sugar
    11.8 -images: 
    11.9 -test: Sugar
   11.10 -
   11.11 -all: images test
   11.12 -
   11.13 -
   11.14 -## global settings
   11.15 -
   11.16 -SRC = $(ISABELLE_HOME)/src
   11.17 -OUT = $(ISABELLE_OUTPUT)
   11.18 -LOG = $(OUT)/log
   11.19 -
   11.20 -USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -g false -d false -D document -M 1
   11.21 -
   11.22 -
   11.23 -## Sugar
   11.24 -
   11.25 -Sugar: $(LOG)/HOL-Sugar.gz
   11.26 -
   11.27 -$(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/Sugar.thy \
   11.28 -  Sugar/document/root.tex Sugar/document/root.bib \
   11.29 -  $(SRC)/HOL/Library/LaTeXsugar.thy $(SRC)/HOL/Library/OptionalSugar.thy 
   11.30 -	@$(USEDIR) HOL Sugar
   11.31 -	@rm -f Sugar/document/isabelle.sty Sugar/document/isabellesym.sty \
   11.32 -	 Sugar/document/pdfsetup.sty Sugar/document/session.tex
   11.33 -
   11.34 -
   11.35 -## clean
   11.36 -
   11.37 -clean:
   11.38 -	@rm -f $(LOG)/HOL-Sugar.gz

    12.1 --- a/doc-src/LaTeXsugar/Sugar/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,6 +0,0 @@
    12.4 -no_document use_thys [
    12.5 -  "~~/src/HOL/Library/LaTeXsugar",
    12.6 -  "~~/src/HOL/Library/OptionalSugar"
    12.7 -];
    12.8 -use_thy "Sugar";
    12.9 -

    13.1 --- a/doc-src/Locales/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,37 +0,0 @@
    13.4 -
    13.5 -## targets
    13.6 -
    13.7 -default: Locales
    13.8 -images:
    13.9 -test: Locales
   13.10 -
   13.11 -all: images test
   13.12 -
   13.13 -
   13.14 -## global settings
   13.15 -
   13.16 -SRC = $(ISABELLE_HOME)/src
   13.17 -OUT = $(ISABELLE_OUTPUT)
   13.18 -LOG = $(OUT)/log
   13.19 -USEDIR = $(ISABELLE_TOOL) usedir -d false -D document
   13.20 -
   13.21 -
   13.22 -## Locales
   13.23 -
   13.24 -Locales: $(LOG)/HOL-Locales.gz
   13.25 -
   13.26 -HOL:
   13.27 -	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
   13.28 -
   13.29 -$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Examples.thy \
   13.30 -  Locales/Examples1.thy Locales/Examples2.thy Locales/Examples3.thy \
   13.31 -  Locales/document/root.tex Locales/document/root.bib
   13.32 -	@$(USEDIR) $(OUT)/HOL Locales
   13.33 -	@rm -f Locales/document/isabelle.sty Locales/document/isabellesym.sty \
   13.34 -	 Locales/document/pdfsetup.sty
   13.35 -
   13.36 -
   13.37 -## clean
   13.38 -
   13.39 -clean:
   13.40 -	@rm -f $(LOG)/HOL-Locales.gz

    14.1 --- a/doc-src/Locales/Locales/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,3 +0,0 @@
    14.4 -use_thy "Examples1";
    14.5 -use_thy "Examples2";
    14.6 -use_thy "Examples3";

    15.1 --- a/doc-src/Main/Docs/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,1 +0,0 @@
    15.4 -use_thy "Main_Doc";

    16.1 --- a/doc-src/Main/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,35 +0,0 @@
    16.4 -
    16.5 -## targets
    16.6 -
    16.7 -default: HOL-Docs
    16.8 -images:
    16.9 -test: HOL-Docs
   16.10 -
   16.11 -all: images test
   16.12 -
   16.13 -
   16.14 -## global settings
   16.15 -
   16.16 -SRC = $(ISABELLE_HOME)/src
   16.17 -OUT = $(ISABELLE_OUTPUT)
   16.18 -LOG = $(OUT)/log
   16.19 -
   16.20 -USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
   16.21 -
   16.22 -
   16.23 -## sessions
   16.24 -
   16.25 -HOL-Docs: $(LOG)/HOL-Docs.gz
   16.26 -
   16.27 -$(LOG)/HOL-Docs.gz: Docs/Main_Doc.thy Docs/ROOT.ML
   16.28 -	@$(USEDIR) HOL Docs
   16.29 -	@rm -f Docs/document/isabelle.sty
   16.30 -	@rm -f Docs/document/isabellesym.sty
   16.31 -	@rm -f Docs/document/pdfsetup.sty
   16.32 -	@rm -f Docs/document/session.tex
   16.33 -
   16.34 -
   16.35 -## clean
   16.36 -
   16.37 -clean:
   16.38 -	@rm -f $(LOG)/HOL-Docs.gz

    17.1 --- a/doc-src/ProgProve/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,44 +0,0 @@
    17.4 -## targets
    17.5 -
    17.6 -default: HOL-ProgProve
    17.7 -images:
    17.8 -test: HOL-ProgProve
    17.9 -
   17.10 -all: images test
   17.11 -
   17.12 -
   17.13 -## global settings
   17.14 -
   17.15 -SRC = $(ISABELLE_HOME)/src
   17.16 -OUT = $(ISABELLE_OUTPUT)
   17.17 -LOG = $(OUT)/log
   17.18 -
   17.19 -USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
   17.20 -
   17.21 -
   17.22 -## sessions
   17.23 -
   17.24 -HOL-ProgProve: $(LOG)/HOL-ProgProve.gz
   17.25 -
   17.26 -$(LOG)/HOL-ProgProve.gz: \
   17.27 -  Thys/Basics.thy \
   17.28 -  Thys/Bool_nat_list.thy \
   17.29 -  Thys/Isar.thy \
   17.30 -  Thys/LaTeXsugar.thy \
   17.31 -  Thys/Logic.thy \
   17.32 -  Thys/MyList.thy \
   17.33 -  Thys/Types_and_funs.thy \
   17.34 -  Thys/ROOT.ML
   17.35 -	@$(USEDIR) -s ProgProve HOL Thys
   17.36 -	@rm -f Thys/document/MyList.tex
   17.37 -	@rm -f Thys/document/isabelle.sty
   17.38 -	@rm -f Thys/document/isabellesym.sty
   17.39 -	@rm -f Thys/document/pdfsetup.sty
   17.40 -	@rm -f Thys/document/railsetup.sty
   17.41 -	@rm -f Thys/document/session.tex
   17.42 -
   17.43 -
   17.44 -## clean
   17.45 -
   17.46 -clean:
   17.47 -	@rm -f $(LOG)/HOL-ProgProve.gz

    18.1 --- a/doc-src/ProgProve/Thys/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,10 +0,0 @@
    18.4 -Printer.show_question_marks_default := false;
    18.5 -
    18.6 -use_thys [
    18.7 - "Basics",
    18.8 - "Bool_nat_list",
    18.9 - "MyList",
   18.10 - "Types_and_funs",
   18.11 - "Logic",
   18.12 - "Isar"
   18.13 -];

    19.1 --- a/doc-src/System/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,35 +0,0 @@
    19.4 -
    19.5 -## targets
    19.6 -
    19.7 -default: Pure-System
    19.8 -images: 
    19.9 -test: Pure-System
   19.10 -
   19.11 -all: images test
   19.12 -
   19.13 -
   19.14 -## global settings
   19.15 -
   19.16 -SRC = $(ISABELLE_HOME)/src
   19.17 -OUT = $(ISABELLE_OUTPUT)
   19.18 -LOG = $(OUT)/log
   19.19 -
   19.20 -USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
   19.21 -
   19.22 -
   19.23 -## sessions
   19.24 -
   19.25 -Pure-System: $(LOG)/Pure-System.gz
   19.26 -
   19.27 -$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/Base.thy	\
   19.28 -  Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy	\
   19.29 -  Thy/Scala.thy Thy/Sessions.thy
   19.30 -	@$(USEDIR) -s System Pure Thy
   19.31 -	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
   19.32 -	 Thy/document/pdfsetup.sty Thy/document/session.tex
   19.33 -
   19.34 -
   19.35 -## clean
   19.36 -
   19.37 -clean:
   19.38 -	@rm -f $(LOG)/Pure-System.gz

    20.1 --- a/doc-src/System/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,1 +0,0 @@
    20.4 -use_thys ["Basics", "Interfaces", "Scala", "Sessions", "Presentation", "Misc"];

    21.1 --- a/doc-src/TutorialI/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,66 +0,0 @@
    21.4 -#
    21.5 -# IsaMakefile for Tutorial
    21.6 -#
    21.7 -
    21.8 -## targets
    21.9 -
   21.10 -default: HOL-Tutorial HOL-ToyList2
   21.11 -images:
   21.12 -test:
   21.13 -all: default
   21.14 -
   21.15 -
   21.16 -## global settings
   21.17 -
   21.18 -SRC = $(ISABELLE_HOME)/src
   21.19 -OUT = $(ISABELLE_OUTPUT)
   21.20 -LOG = $(OUT)/log
   21.21 -OPTIONS = -m brackets -i true -d "" -D document -M 1
   21.22 -USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS)
   21.23 -
   21.24 -
   21.25 -## HOL
   21.26 -
   21.27 -HOL:
   21.28 -	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
   21.29 -
   21.30 -
   21.31 -## HOL-Tutorial
   21.32 -
   21.33 -HOL-Tutorial: HOL $(LOG)/HOL-Tutorial.gz
   21.34 -
   21.35 -$(LOG)/HOL-Tutorial.gz: $(OUT)/HOL ROOT.ML Ifexpr/Ifexpr.thy		\
   21.36 -  ToyList2/ToyList.thy CodeGen/CodeGen.thy Datatype/ABexpr.thy		\
   21.37 -  Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy	\
   21.38 -  Trie/Trie.thy Fun/fun0.thy Advanced/simp2.thy Rules/Basic.thy		\
   21.39 -  Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy	\
   21.40 -  Rules/Tacticals.thy Rules/find2.thy Sets/Examples.thy			\
   21.41 -  Sets/Functions.thy Sets/Recur.thy Sets/Relations.thy CTL/Base.thy	\
   21.42 -  CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy Inductive/Even.thy		\
   21.43 -  Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy		\
   21.44 -  Inductive/Advanced.thy Types/Numbers.thy Types/Pairs.thy		\
   21.45 -  Types/Records.thy Types/Typedefs.thy Types/Overloading.thy		\
   21.46 -  Types/Axioms.thy Misc/Tree.thy Misc/Tree2.thy Misc/Plus.thy		\
   21.47 -  Misc/fakenat.thy Misc/natsum.thy Misc/pairs2.thy Misc/Option2.thy	\
   21.48 -  Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy Misc/simp.thy	\
   21.49 -  Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy			\
   21.50 -  Protocol/Message.thy Protocol/Event.thy Protocol/Public.thy		\
   21.51 -  Protocol/NS_Public.thy Documents/Documents.thy
   21.52 -	$(USEDIR) -s Tutorial $(OUT)/HOL .
   21.53 -
   21.54 -
   21.55 -## HOL-ToyList2
   21.56 -
   21.57 -HOL-ToyList2: HOL $(LOG)/HOL-ToyList2.gz
   21.58 -
   21.59 -ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
   21.60 -	cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
   21.61 -
   21.62 -$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ROOT.ML
   21.63 -	$(USEDIR) $(OUT)/HOL ToyList2
   21.64 -
   21.65 -
   21.66 -## clean
   21.67 -
   21.68 -clean:
   21.69 -	@rm -f tutorial.dvi $(LOG)/HOL-Tutorial.gz $(LOG)/HOL-ToyList2.gz

    22.1 --- a/doc-src/TutorialI/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,71 +0,0 @@
    22.4 -Thy_Output.indent_default := 5;
    22.5 -
    22.6 -use_thy "ToyList/ToyList";
    22.7 -
    22.8 -use_thy "Ifexpr/Ifexpr";
    22.9 -
   22.10 -use_thy "CodeGen/CodeGen";
   22.11 -
   22.12 -use_thy "Trie/Trie";
   22.13 -
   22.14 -use_thy "Datatype/ABexpr";
   22.15 -use_thy "Datatype/unfoldnested";
   22.16 -use_thy "Datatype/Nested";
   22.17 -use_thy "Datatype/Fundata";
   22.18 -
   22.19 -use_thy "Fun/fun0";
   22.20 -
   22.21 -use_thy "Advanced/simp2";
   22.22 -
   22.23 -use_thy "CTL/PDL";
   22.24 -use_thy "CTL/CTL";
   22.25 -use_thy "CTL/CTLind";
   22.26 -
   22.27 -use_thy "Inductive/Even";
   22.28 -use_thy "Inductive/Mutual";
   22.29 -use_thy "Inductive/Star";
   22.30 -use_thy "Inductive/AB";
   22.31 -use_thy "Inductive/Advanced";
   22.32 -
   22.33 -use_thy "Misc/Tree";
   22.34 -use_thy "Misc/Tree2";
   22.35 -use_thy "Misc/Plus";
   22.36 -use_thy "Misc/case_exprs";
   22.37 -use_thy "Misc/fakenat";
   22.38 -use_thy "Misc/natsum";
   22.39 -use_thy "Misc/pairs2";
   22.40 -use_thy "Misc/Option2";
   22.41 -use_thy "Misc/types";
   22.42 -use_thy "Misc/prime_def";
   22.43 -use_thy "Misc/simp";
   22.44 -use_thy "Misc/Itrev";
   22.45 -use_thy "Misc/AdvancedInd";
   22.46 -use_thy "Misc/appendix";
   22.47 -
   22.48 -
   22.49 -Thy_Output.indent_default := 0;
   22.50 -
   22.51 -use_thy "Protocol/NS_Public";
   22.52 -
   22.53 -use_thy "Documents/Documents";
   22.54 -
   22.55 -no_document use_thy "Types/Setup";
   22.56 -use_thy "Types/Numbers";
   22.57 -use_thy "Types/Pairs";
   22.58 -use_thy "Types/Records";
   22.59 -use_thy "Types/Typedefs";
   22.60 -use_thy "Types/Overloading";
   22.61 -use_thy "Types/Axioms";
   22.62 -
   22.63 -use_thy "Rules/Basic";
   22.64 -use_thy "Rules/Blast";
   22.65 -use_thy "Rules/Force";
   22.66 -use_thy "Rules/Forward";
   22.67 -use_thy "Rules/Tacticals";
   22.68 -use_thy "Rules/find2";
   22.69 -
   22.70 -use_thy "Sets/Examples";
   22.71 -use_thy "Sets/Functions";
   22.72 -use_thy "Sets/Relations";
   22.73 -use_thy "Sets/Recur";
   22.74 -

    23.1 --- a/doc-src/TutorialI/ToyList2/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,1 +0,0 @@
    23.4 -use_thy "ToyList";

    24.1 --- a/doc-src/ZF/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,42 +0,0 @@
    24.4 -#
    24.5 -# IsaMakefile to build the examples for the FOL and ZF manual
    24.6 -#
    24.7 -
    24.8 -## targets
    24.9 -
   24.10 -default: ZF-examples
   24.11 -images:
   24.12 -test:
   24.13 -all: default
   24.14 -
   24.15 -
   24.16 -## global settings
   24.17 -
   24.18 -SRC = $(ISABELLE_HOME)/src
   24.19 -OUT = $(ISABELLE_OUTPUT)
   24.20 -LOG = $(OUT)/log
   24.21 -USEDIR = @$(ISABELLE_TOOL) usedir -m brackets -i true -d "" -D document
   24.22 -
   24.23 -
   24.24 -## ZF
   24.25 -
   24.26 -ZF:
   24.27 -	@cd $(SRC)/ZF; $(ISABELLE_TOOL) make ZF
   24.28 -
   24.29 -
   24.30 -## ZF-examples
   24.31 -
   24.32 -ZF-examples: ZF $(LOG)/ZF-examples.gz
   24.33 -
   24.34 -$(LOG)/ZF-examples.gz: $(OUT)/ZF \
   24.35 -	FOL_examples.thy  IFOL_examples.thy ZF_examples.thy If.thy ROOT.ML 
   24.36 -	@$(USEDIR) -s examples $(OUT)/ZF .
   24.37 -	@rm -f document/isabelle.sty
   24.38 -	@rm -f document/isabellesym.sty
   24.39 -	@rm -f document/pdfsetup.sty
   24.40 -	@rm -f document/session.tex
   24.41 -
   24.42 -## clean
   24.43 -
   24.44 -clean:
   24.45 -	@rm -f $(LOG)/ZF-examples.gz document/*.tex 

    25.1 --- a/doc-src/ZF/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,4 +0,0 @@
    25.4 -use_thy "IFOL_examples";
    25.5 -use_thy "FOL_examples";
    25.6 -use_thy "ZF_examples";
    25.7 -use_thy "If";