formal Base theory;

--- a/doc-src/IsarRef/IsaMakefile	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/IsaMakefile	Tue May 03 15:07:36 2011 +0200
@@ -21,7 +21,7 @@
 
 HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
 
-$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML		\
+$(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/Introduction.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy	\
   Thy/Misc.thy Thy/Document_Preparation.thy Thy/Generic.thy		\
@@ -35,7 +35,7 @@
 HOLCF-IsarRef: $(LOG)/HOLCF-IsarRef.gz
 
 $(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML	\
-  Thy/HOLCF_Specific.thy
+  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
@@ -43,8 +43,8 @@
 
 ZF-IsarRef: $(LOG)/ZF-IsarRef.gz
 
-$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML 		\
-  Thy/ZF_Specific.thy
+$(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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/Base.thy	Tue May 03 15:07:36 2011 +0200
@@ -0,0 +1,12 @@
+theory Base
+imports Pure
+uses "../../antiquote_setup.ML"
+begin
+
+setup {*
+  member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup
+*}
+
+declare [[thy_output_source]]
+
+end

--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory Document_Preparation
-imports Main
+imports Base Main
 begin
 
 chapter {* Document preparation \label{ch:document-prep} *}

--- a/doc-src/IsarRef/Thy/First_Order_Logic.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy	Tue May 03 15:07:36 2011 +0200
@@ -2,7 +2,7 @@
 header {* Example: First-Order Logic *}
 
 theory %visible First_Order_Logic
-imports Pure
+imports Base  (* FIXME Pure!? *)
 begin
 
 text {*

--- a/doc-src/IsarRef/Thy/Framework.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/Framework.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory Framework
-imports Main
+imports Base Main
 begin
 
 chapter {* The Isabelle/Isar Framework \label{ch:isar-framework} *}

--- a/doc-src/IsarRef/Thy/Generic.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory Generic
-imports Main
+imports Base Main
 begin
 
 chapter {* Generic tools and packages \label{ch:gen-tools} *}

--- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory HOLCF_Specific
-imports HOLCF
+imports Base HOLCF
 begin
 
 chapter {* Isabelle/HOLCF \label{ch:holcf} *}

--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory HOL_Specific
-imports Main
+imports Base Main
 begin
 
 chapter {* Isabelle/HOL \label{ch:hol} *}

--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory Inner_Syntax
-imports Main
+imports Base Main
 begin
 
 chapter {* Inner syntax --- the term language \label{ch:inner-syntax} *}

--- a/doc-src/IsarRef/Thy/Introduction.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/Introduction.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory Introduction
-imports Main
+imports Base Main
 begin
 
 chapter {* Introduction *}

--- a/doc-src/IsarRef/Thy/ML_Tactic.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/ML_Tactic.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory ML_Tactic
-imports Main
+imports Base Main
 begin
 
 chapter {* ML tactic expressions *}

--- a/doc-src/IsarRef/Thy/Misc.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/Misc.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory Misc
-imports Main
+imports Base Main
 begin
 
 chapter {* Other commands *}

--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory Outer_Syntax
-imports Main
+imports Base Main
 begin
 
 chapter {* Outer syntax *}

--- a/doc-src/IsarRef/Thy/Proof.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory Proof
-imports Main
+imports Base Main
 begin
 
 chapter {* Proofs \label{ch:proofs} *}

--- a/doc-src/IsarRef/Thy/Quick_Reference.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/Quick_Reference.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory Quick_Reference
-imports Main
+imports Base Main
 begin
 
 chapter {* Isabelle/Isar quick reference \label{ap:refcard} *}

--- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Tue May 03 15:07:36 2011 +0200
@@ -1,4 +1,3 @@
-Thy_Output.source_default := true;
-use "../../antiquote_setup.ML";
+quick_and_dirty := true;
 
 use_thy "HOLCF_Specific";

--- a/doc-src/IsarRef/Thy/ROOT-ZF.ML	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML	Tue May 03 15:07:36 2011 +0200
@@ -1,4 +1,3 @@
-Thy_Output.source_default := true;
-use "../../antiquote_setup.ML";
+quick_and_dirty := true;
 
 use_thy "ZF_Specific";

--- a/doc-src/IsarRef/Thy/ROOT.ML	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML	Tue May 03 15:07:36 2011 +0200
@@ -1,6 +1,4 @@
 quick_and_dirty := true;
-Thy_Output.source_default := true;
-use "../../antiquote_setup.ML";
 
 use_thys [
   "Introduction",

--- a/doc-src/IsarRef/Thy/Spec.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory Spec
-imports Main
+imports Base Main
 begin
 
 chapter {* Theory specifications *}

--- a/doc-src/IsarRef/Thy/Symbols.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/Symbols.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory Symbols
-imports Pure
+imports Base Main
 begin
 
 chapter {* Predefined Isabelle symbols \label{app:symbols} *}

--- a/doc-src/IsarRef/Thy/ZF_Specific.thy	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Tue May 03 15:07:36 2011 +0200
@@ -1,5 +1,5 @@
 theory ZF_Specific
-imports Main
+imports Base Main
 begin
 
 chapter {* Isabelle/ZF \label{ch:zf} *}

--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Document{\isaliteral{5F}{\isacharunderscore}}Preparation\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Tue May 03 15:07:36 2011 +0200
@@ -13,7 +13,7 @@
 \isatagvisible
 \isacommand{theory}\isamarkupfalse%
 \ First{\isaliteral{5F}{\isacharunderscore}}Order{\isaliteral{5F}{\isacharunderscore}}Logic\isanewline
-\isakeyword{imports}\ Pure\isanewline
+\isakeyword{imports}\ Base\ \ \isanewline
 \isakeyword{begin}%
 \endisatagvisible
 {\isafoldvisible}%

--- a/doc-src/IsarRef/Thy/document/Framework.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Framework.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Framework\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/Generic.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Generic\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ HOLCF{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
-\isakeyword{imports}\ HOLCF\isanewline
+\isakeyword{imports}\ Base\ HOLCF\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Inner{\isaliteral{5F}{\isacharunderscore}}Syntax\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/Introduction.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Introduction.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Introduction\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ ML{\isaliteral{5F}{\isacharunderscore}}Tactic\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/Misc.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Misc.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Misc\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Outer{\isaliteral{5F}{\isacharunderscore}}Syntax\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/Proof.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Proof\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Quick{\isaliteral{5F}{\isacharunderscore}}Reference\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/Spec.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Spec\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/Symbols.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Symbols.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Symbols\isanewline
-\isakeyword{imports}\ Pure\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%

--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Tue May 03 14:23:40 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Tue May 03 15:07:36 2011 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ ZF{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
-\isakeyword{imports}\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%