# HG changeset patch
# User wenzelm
# Date 1608760983 -3600
# Node ID d0a0b74f0ad70d77e3a58ac4bd4833e79fd774cb
# Parent  db8f94656024ebc496d839e6506acba8285339eb
avoid multiple uses of the same ML file;

diff -r db8f94656024 -r d0a0b74f0ad7 src/Doc/ROOT
--- a/src/Doc/ROOT	Wed Dec 23 22:25:22 2020 +0100
+++ b/src/Doc/ROOT	Wed Dec 23 23:03:03 2020 +0100
@@ -405,6 +405,8 @@
   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
     "Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
+  theories [document = false]
+    Base
   theories [threads = 1]
     "ToyList/ToyList_Test"
   theories [thy_output_indent = 5]
@@ -443,8 +445,6 @@
   theories
     "Protocol/NS_Public"
     "Documents/Documents"
-  theories [document = false]
-    "Types/Setup"
   theories [thy_output_margin = 64, thy_output_indent = 0]
     "Types/Numbers"
     "Types/Pairs"
diff -r db8f94656024 -r d0a0b74f0ad7 src/Doc/Tutorial/Inductive/Advanced.thy
--- a/src/Doc/Tutorial/Inductive/Advanced.thy	Wed Dec 23 22:25:22 2020 +0100
+++ b/src/Doc/Tutorial/Inductive/Advanced.thy	Wed Dec 23 23:03:03 2020 +0100
@@ -1,6 +1,4 @@
-(*<*)theory Advanced imports Even begin
-ML_file \<open>../../antiquote_setup.ML\<close>
-(*>*)
+(*<*)theory Advanced imports Even begin(*>*)
 
 text \<open>
 The premises of introduction rules may contain universal quantifiers and
diff -r db8f94656024 -r d0a0b74f0ad7 src/Doc/Tutorial/Inductive/Even.thy
--- a/src/Doc/Tutorial/Inductive/Even.thy	Wed Dec 23 22:25:22 2020 +0100
+++ b/src/Doc/Tutorial/Inductive/Even.thy	Wed Dec 23 23:03:03 2020 +0100
@@ -1,6 +1,4 @@
-(*<*)theory Even imports Main begin
-ML_file \<open>../../antiquote_setup.ML\<close> 
-(*>*)
+(*<*)theory Even imports "../Setup" begin(*>*)
 
 section\<open>The Set of Even Numbers\<close>
 
diff -r db8f94656024 -r d0a0b74f0ad7 src/Doc/Tutorial/Protocol/Message.thy
--- a/src/Doc/Tutorial/Protocol/Message.thy	Wed Dec 23 22:25:22 2020 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Wed Dec 23 23:03:03 2020 +0100
@@ -7,8 +7,7 @@
 
 section\<open>Theory of Agents and Messages for Security Protocols\<close>
 
-theory Message imports Main begin
-ML_file \<open>../../antiquote_setup.ML\<close>
+theory Message imports "../Setup" begin
 
 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
diff -r db8f94656024 -r d0a0b74f0ad7 src/Doc/Tutorial/Setup.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/Setup.thy	Wed Dec 23 23:03:03 2020 +0100
@@ -0,0 +1,10 @@
+(*:maxLineLen=78:*)
+
+theory Setup
+imports Main
+begin
+
+ML_file \<open>../antiquote_setup.ML\<close>
+ML_file \<open>../more_antiquote.ML\<close>
+
+end
diff -r db8f94656024 -r d0a0b74f0ad7 src/Doc/Tutorial/Types/Axioms.thy
--- a/src/Doc/Tutorial/Types/Axioms.thy	Wed Dec 23 22:25:22 2020 +0100
+++ b/src/Doc/Tutorial/Types/Axioms.thy	Wed Dec 23 23:03:03 2020 +0100
@@ -1,4 +1,4 @@
-(*<*)theory Axioms imports Overloading Setup begin(*>*)
+(*<*)theory Axioms imports Overloading "../Setup" begin(*>*)
 
 subsection \<open>Axioms\<close>
 
diff -r db8f94656024 -r d0a0b74f0ad7 src/Doc/Tutorial/Types/Overloading.thy
--- a/src/Doc/Tutorial/Types/Overloading.thy	Wed Dec 23 22:25:22 2020 +0100
+++ b/src/Doc/Tutorial/Types/Overloading.thy	Wed Dec 23 23:03:03 2020 +0100
@@ -1,4 +1,4 @@
-(*<*)theory Overloading imports Main Setup begin
+(*<*)theory Overloading imports "../Setup" begin
 
 hide_class (open) plus (*>*)
 
diff -r db8f94656024 -r d0a0b74f0ad7 src/Doc/Tutorial/Types/Setup.thy
--- a/src/Doc/Tutorial/Types/Setup.thy	Wed Dec 23 22:25:22 2020 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-theory Setup
-imports Main
-begin
-
-ML_file \<open>../../antiquote_setup.ML\<close>
-ML_file \<open>../../more_antiquote.ML\<close>
-
-end