# HG changeset patch
# User wenzelm
# Date 1343660843 -7200
# Node ID 0095de9e9da0878f97a13f6b7b98785202a4ec22
# Parent  0090fab725e3a71ae902164ffe4acb8d21231f25
removed obsolete IsaMakefile + ROOT.ML setup -- doc-src is managed via isabelle build;

diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/Classes/IsaMakefile
--- a/doc-src/Classes/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-
-## targets
-
-default: Thy
-images: 
-test: Thy
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
-
-
-## Thy
-
-THY = $(LOG)/HOL-Thy.gz
-
-Thy: $(THY)
-
-$(THY): $(OUT)/HOL Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy ../antiquote_setup.ML ../more_antiquote.ML
-	@$(USEDIR) HOL Thy
-	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
-	  Thy/document/pdfsetup.sty Thy/document/session.tex
-
-
-## clean
-
-clean:
-	@rm -f $(THY)
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/Classes/Thy/ROOT.ML
--- a/doc-src/Classes/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-no_document use_thy "Setup";
-use_thy "Classes";
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/Codegen/IsaMakefile
--- a/doc-src/Codegen/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-
-## targets
-
-default: Thy
-images: 
-test: Thy
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
-
-
-## Thy
-
-THY = $(LOG)/HOL-Thy.gz
-
-Thy: $(THY)
-
-$(THY): $(OUT)/HOL-Library Thy/ROOT.ML Thy/*.thy ../antiquote_setup.ML ../more_antiquote.ML
-	@$(USEDIR) -m no_brackets -m iff HOL-Library Thy
-	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
-	  Thy/document/pdfsetup.sty Thy/document/session.tex
-
-
-## clean
-
-clean:
-	@rm -f $(THY)
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/Codegen/Thy/ROOT.ML
--- a/doc-src/Codegen/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-
-no_document use_thy "Setup";
-
-use_thy "Introduction";
-use_thy "Foundations";
-use_thy "Refinement";
-use_thy "Inductive_Predicate";
-use_thy "Evaluation";
-use_thy "Adaptation";
-use_thy "Further";
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/Functions/IsaMakefile
--- a/doc-src/Functions/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-
-## targets
-
-default: Thy
-images: 
-test: Thy
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
-
-
-## Thy
-
-THY = $(LOG)/HOL-Thy.gz
-
-Thy: $(THY)
-
-$(THY): $(OUT)/HOL Thy/ROOT.ML Thy/Functions.thy
-	@$(USEDIR) HOL Thy
-	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
-	 Thy/document/pdfsetup.sty Thy/document/session.tex
-
-
-## clean
-
-clean:
-	@rm -f $(THY)
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/Functions/Thy/ROOT.ML
--- a/doc-src/Functions/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thy "Functions";
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/IsarImplementation/IsaMakefile
--- a/doc-src/IsarImplementation/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-
-## targets
-
-default: Thy
-images: 
-test: Thy
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
-
-
-## sessions
-
-Thy: $(LOG)/HOL-Thy.gz
-
-$(LOG)/HOL-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Eq.thy			\
-  Thy/Integration.thy Thy/Isar.thy Thy/Local_Theory.thy Thy/Logic.thy	\
-  Thy/Prelim.thy Thy/Proof.thy Thy/Syntax.thy Thy/Tactic.thy		\
-  Thy/ML.thy ../antiquote_setup.ML
-	@$(USEDIR) HOL Thy
-	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
-	 Thy/document/pdfsetup.sty Thy/document/session.tex
-
-
-## clean
-
-clean:
-	@rm -f $(LOG)/HOL-Thy.gz
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/IsarImplementation/Thy/ROOT.ML
--- a/doc-src/IsarImplementation/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-use_thys [
-  "Eq",
-  "Integration",
-  "Isar",
-  "Local_Theory",
-  "Logic",
-  "ML",
-  "Prelim",
-  "Proof",
-  "Syntax",
-  "Tactic"
-];
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/IsarRef/IsaMakefile
--- a/doc-src/IsarRef/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-
-## targets
-
-default: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
-images: 
-test: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
-
-
-## sessions
-
-HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
-
-$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/Base.thy	\
-  Thy/First_Order_Logic.thy Thy/Framework.thy Thy/Inner_Syntax.thy	\
-  Thy/Preface.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy	\
-  Thy/Misc.thy Thy/Document_Preparation.thy Thy/Generic.thy		\
-  Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/Synopsis.thy		\
-  Thy/Symbols.thy Thy/ML_Tactic.thy
-	@$(USEDIR) -s IsarRef HOL Thy
-	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
-	 Thy/document/pdfsetup.sty Thy/document/session.tex
-
-
-HOLCF-IsarRef: $(LOG)/HOLCF-IsarRef.gz
-
-$(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML	\
-  Thy/Base.thy Thy/HOLCF_Specific.thy
-	@$(USEDIR) -s IsarRef -f ROOT-HOLCF.ML HOLCF Thy
-	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
-	 Thy/document/pdfsetup.sty Thy/document/session.tex
-
-
-ZF-IsarRef: $(LOG)/ZF-IsarRef.gz
-
-$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML	\
-  Thy/Base.thy Thy/ZF_Specific.thy
-	@$(USEDIR) -s IsarRef -f ROOT-ZF.ML ZF Thy
-	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
-	 Thy/document/pdfsetup.sty Thy/document/session.tex
-
-
-## clean
-
-clean:
-	@rm -f $(LOG)/HOL-IsarRef.gz $(LOG)/HOLCF-IsarRef.gz $(LOG)/ZF-IsarRef.gz
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/IsarRef/Thy/ROOT.ML
--- a/doc-src/IsarRef/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-quick_and_dirty := true;
-
-use_thys [
-  "Preface",
-  "Synopsis",
-  "Framework",
-  "First_Order_Logic",
-  "Outer_Syntax",
-  "Document_Preparation",
-  "Spec",
-  "Proof",
-  "Inner_Syntax",
-  "Misc",
-  "Generic",
-  "HOL_Specific",
-  "Quick_Reference",
-  "Symbols",
-  "ML_Tactic"
-];
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/LaTeXsugar/IsaMakefile
--- a/doc-src/LaTeXsugar/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-
-## targets
-
-default: Sugar
-images: 
-test: Sugar
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -g false -d false -D document -M 1
-
-
-## Sugar
-
-Sugar: $(LOG)/HOL-Sugar.gz
-
-$(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/Sugar.thy \
-  Sugar/document/root.tex Sugar/document/root.bib \
-  $(SRC)/HOL/Library/LaTeXsugar.thy $(SRC)/HOL/Library/OptionalSugar.thy 
-	@$(USEDIR) HOL Sugar
-	@rm -f Sugar/document/isabelle.sty Sugar/document/isabellesym.sty \
-	 Sugar/document/pdfsetup.sty Sugar/document/session.tex
-
-
-## clean
-
-clean:
-	@rm -f $(LOG)/HOL-Sugar.gz
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/LaTeXsugar/Sugar/ROOT.ML
--- a/doc-src/LaTeXsugar/Sugar/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-no_document use_thys [
-  "~~/src/HOL/Library/LaTeXsugar",
-  "~~/src/HOL/Library/OptionalSugar"
-];
-use_thy "Sugar";
-
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/Locales/IsaMakefile
--- a/doc-src/Locales/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-
-## targets
-
-default: Locales
-images:
-test: Locales
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-USEDIR = $(ISABELLE_TOOL) usedir -d false -D document
-
-
-## Locales
-
-Locales: $(LOG)/HOL-Locales.gz
-
-HOL:
-	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
-
-$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Examples.thy \
-  Locales/Examples1.thy Locales/Examples2.thy Locales/Examples3.thy \
-  Locales/document/root.tex Locales/document/root.bib
-	@$(USEDIR) $(OUT)/HOL Locales
-	@rm -f Locales/document/isabelle.sty Locales/document/isabellesym.sty \
-	 Locales/document/pdfsetup.sty
-
-
-## clean
-
-clean:
-	@rm -f $(LOG)/HOL-Locales.gz
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/Locales/Locales/ROOT.ML
--- a/doc-src/Locales/Locales/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-use_thy "Examples1";
-use_thy "Examples2";
-use_thy "Examples3";
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/Main/Docs/ROOT.ML
--- a/doc-src/Main/Docs/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thy "Main_Doc";
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/Main/IsaMakefile
--- a/doc-src/Main/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-
-## targets
-
-default: HOL-Docs
-images:
-test: HOL-Docs
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
-
-
-## sessions
-
-HOL-Docs: $(LOG)/HOL-Docs.gz
-
-$(LOG)/HOL-Docs.gz: Docs/Main_Doc.thy Docs/ROOT.ML
-	@$(USEDIR) HOL Docs
-	@rm -f Docs/document/isabelle.sty
-	@rm -f Docs/document/isabellesym.sty
-	@rm -f Docs/document/pdfsetup.sty
-	@rm -f Docs/document/session.tex
-
-
-## clean
-
-clean:
-	@rm -f $(LOG)/HOL-Docs.gz
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/ProgProve/IsaMakefile
--- a/doc-src/ProgProve/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-## targets
-
-default: HOL-ProgProve
-images:
-test: HOL-ProgProve
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
-
-
-## sessions
-
-HOL-ProgProve: $(LOG)/HOL-ProgProve.gz
-
-$(LOG)/HOL-ProgProve.gz: \
-  Thys/Basics.thy \
-  Thys/Bool_nat_list.thy \
-  Thys/Isar.thy \
-  Thys/LaTeXsugar.thy \
-  Thys/Logic.thy \
-  Thys/MyList.thy \
-  Thys/Types_and_funs.thy \
-  Thys/ROOT.ML
-	@$(USEDIR) -s ProgProve HOL Thys
-	@rm -f Thys/document/MyList.tex
-	@rm -f Thys/document/isabelle.sty
-	@rm -f Thys/document/isabellesym.sty
-	@rm -f Thys/document/pdfsetup.sty
-	@rm -f Thys/document/railsetup.sty
-	@rm -f Thys/document/session.tex
-
-
-## clean
-
-clean:
-	@rm -f $(LOG)/HOL-ProgProve.gz
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/ProgProve/Thys/ROOT.ML
--- a/doc-src/ProgProve/Thys/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-Printer.show_question_marks_default := false;
-
-use_thys [
- "Basics",
- "Bool_nat_list",
- "MyList",
- "Types_and_funs",
- "Logic",
- "Isar"
-];
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/System/IsaMakefile
--- a/doc-src/System/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-
-## targets
-
-default: Pure-System
-images: 
-test: Pure-System
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
-
-
-## sessions
-
-Pure-System: $(LOG)/Pure-System.gz
-
-$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/Base.thy	\
-  Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy	\
-  Thy/Scala.thy Thy/Sessions.thy
-	@$(USEDIR) -s System Pure Thy
-	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
-	 Thy/document/pdfsetup.sty Thy/document/session.tex
-
-
-## clean
-
-clean:
-	@rm -f $(LOG)/Pure-System.gz
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/System/Thy/ROOT.ML
--- a/doc-src/System/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thys ["Basics", "Interfaces", "Scala", "Sessions", "Presentation", "Misc"];
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-#
-# IsaMakefile for Tutorial
-#
-
-## targets
-
-default: HOL-Tutorial HOL-ToyList2
-images:
-test:
-all: default
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-OPTIONS = -m brackets -i true -d "" -D document -M 1
-USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS)
-
-
-## HOL
-
-HOL:
-	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
-
-
-## HOL-Tutorial
-
-HOL-Tutorial: HOL $(LOG)/HOL-Tutorial.gz
-
-$(LOG)/HOL-Tutorial.gz: $(OUT)/HOL ROOT.ML Ifexpr/Ifexpr.thy		\
-  ToyList2/ToyList.thy CodeGen/CodeGen.thy Datatype/ABexpr.thy		\
-  Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy	\
-  Trie/Trie.thy Fun/fun0.thy Advanced/simp2.thy Rules/Basic.thy		\
-  Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy	\
-  Rules/Tacticals.thy Rules/find2.thy Sets/Examples.thy			\
-  Sets/Functions.thy Sets/Recur.thy Sets/Relations.thy CTL/Base.thy	\
-  CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy Inductive/Even.thy		\
-  Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy		\
-  Inductive/Advanced.thy Types/Numbers.thy Types/Pairs.thy		\
-  Types/Records.thy Types/Typedefs.thy Types/Overloading.thy		\
-  Types/Axioms.thy Misc/Tree.thy Misc/Tree2.thy Misc/Plus.thy		\
-  Misc/fakenat.thy Misc/natsum.thy Misc/pairs2.thy Misc/Option2.thy	\
-  Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy Misc/simp.thy	\
-  Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy			\
-  Protocol/Message.thy Protocol/Event.thy Protocol/Public.thy		\
-  Protocol/NS_Public.thy Documents/Documents.thy
-	$(USEDIR) -s Tutorial $(OUT)/HOL .
-
-
-## HOL-ToyList2
-
-HOL-ToyList2: HOL $(LOG)/HOL-ToyList2.gz
-
-ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
-	cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
-
-$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ROOT.ML
-	$(USEDIR) $(OUT)/HOL ToyList2
-
-
-## clean
-
-clean:
-	@rm -f tutorial.dvi $(LOG)/HOL-Tutorial.gz $(LOG)/HOL-ToyList2.gz
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/TutorialI/ROOT.ML
--- a/doc-src/TutorialI/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,71 +0,0 @@
-Thy_Output.indent_default := 5;
-
-use_thy "ToyList/ToyList";
-
-use_thy "Ifexpr/Ifexpr";
-
-use_thy "CodeGen/CodeGen";
-
-use_thy "Trie/Trie";
-
-use_thy "Datatype/ABexpr";
-use_thy "Datatype/unfoldnested";
-use_thy "Datatype/Nested";
-use_thy "Datatype/Fundata";
-
-use_thy "Fun/fun0";
-
-use_thy "Advanced/simp2";
-
-use_thy "CTL/PDL";
-use_thy "CTL/CTL";
-use_thy "CTL/CTLind";
-
-use_thy "Inductive/Even";
-use_thy "Inductive/Mutual";
-use_thy "Inductive/Star";
-use_thy "Inductive/AB";
-use_thy "Inductive/Advanced";
-
-use_thy "Misc/Tree";
-use_thy "Misc/Tree2";
-use_thy "Misc/Plus";
-use_thy "Misc/case_exprs";
-use_thy "Misc/fakenat";
-use_thy "Misc/natsum";
-use_thy "Misc/pairs2";
-use_thy "Misc/Option2";
-use_thy "Misc/types";
-use_thy "Misc/prime_def";
-use_thy "Misc/simp";
-use_thy "Misc/Itrev";
-use_thy "Misc/AdvancedInd";
-use_thy "Misc/appendix";
-
-
-Thy_Output.indent_default := 0;
-
-use_thy "Protocol/NS_Public";
-
-use_thy "Documents/Documents";
-
-no_document use_thy "Types/Setup";
-use_thy "Types/Numbers";
-use_thy "Types/Pairs";
-use_thy "Types/Records";
-use_thy "Types/Typedefs";
-use_thy "Types/Overloading";
-use_thy "Types/Axioms";
-
-use_thy "Rules/Basic";
-use_thy "Rules/Blast";
-use_thy "Rules/Force";
-use_thy "Rules/Forward";
-use_thy "Rules/Tacticals";
-use_thy "Rules/find2";
-
-use_thy "Sets/Examples";
-use_thy "Sets/Functions";
-use_thy "Sets/Relations";
-use_thy "Sets/Recur";
-
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/TutorialI/ToyList2/ROOT.ML
--- a/doc-src/TutorialI/ToyList2/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thy "ToyList";
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/ZF/IsaMakefile
--- a/doc-src/ZF/IsaMakefile	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-#
-# IsaMakefile to build the examples for the FOL and ZF manual
-#
-
-## targets
-
-default: ZF-examples
-images:
-test:
-all: default
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-USEDIR = @$(ISABELLE_TOOL) usedir -m brackets -i true -d "" -D document
-
-
-## ZF
-
-ZF:
-	@cd $(SRC)/ZF; $(ISABELLE_TOOL) make ZF
-
-
-## ZF-examples
-
-ZF-examples: ZF $(LOG)/ZF-examples.gz
-
-$(LOG)/ZF-examples.gz: $(OUT)/ZF \
-	FOL_examples.thy  IFOL_examples.thy ZF_examples.thy If.thy ROOT.ML 
-	@$(USEDIR) -s examples $(OUT)/ZF .
-	@rm -f document/isabelle.sty
-	@rm -f document/isabellesym.sty
-	@rm -f document/pdfsetup.sty
-	@rm -f document/session.tex
-
-## clean
-
-clean:
-	@rm -f $(LOG)/ZF-examples.gz document/*.tex 
diff -r 0090fab725e3 -r 0095de9e9da0 doc-src/ZF/ROOT.ML
--- a/doc-src/ZF/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-use_thy "IFOL_examples";
-use_thy "FOL_examples";
-use_thy "ZF_examples";
-use_thy "If";