--- a/doc-src/IsarImplementation/Thy/document/Base.tex Wed Aug 22 23:23:48 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Base.tex Wed Aug 22 23:45:49 2012 +0200
@@ -10,7 +10,6 @@
\isacommand{theory}\isamarkupfalse%
\ Base\isanewline
\isakeyword{imports}\ Main\isanewline
-\isakeyword{uses}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
@@ -26,6 +25,8 @@
\endisadelimML
%
\isatagML
+\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isacommand{setup}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
--- a/doc-src/System/Thy/document/Base.tex Wed Aug 22 23:23:48 2012 +0200
+++ b/doc-src/System/Thy/document/Base.tex Wed Aug 22 23:45:49 2012 +0200
@@ -10,7 +10,6 @@
\isacommand{theory}\isamarkupfalse%
\ Base\isanewline
\isakeyword{imports}\ Pure\isanewline
-\isakeyword{uses}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
@@ -26,8 +25,10 @@
\endisadelimML
%
\isatagML
+\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isacommand{setup}\isamarkupfalse%
-\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
+\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup%
\endisatagML
{\isafoldML}%
%
--- a/doc-src/TutorialI/Inductive/Advanced.thy Wed Aug 22 23:23:48 2012 +0200
+++ b/doc-src/TutorialI/Inductive/Advanced.thy Wed Aug 22 23:45:49 2012 +0200
@@ -1,5 +1,6 @@
-(*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin
-setup {* Antiquote_Setup.setup *}
+(*<*)theory Advanced imports Even begin
+ML_file "../../antiquote_setup.ML"
+setup Antiquote_Setup.setup
(*>*)
text {*
--- a/doc-src/TutorialI/Inductive/Even.thy Wed Aug 22 23:23:48 2012 +0200
+++ b/doc-src/TutorialI/Inductive/Even.thy Wed Aug 22 23:45:49 2012 +0200
@@ -1,5 +1,6 @@
-(*<*)theory Even imports Main uses "../../antiquote_setup.ML" begin
-setup {* Antiquote_Setup.setup *}
+(*<*)theory Even imports Main begin
+ML_file "../../antiquote_setup.ML"
+setup Antiquote_Setup.setup
(*>*)
section{* The Set of Even Numbers *}
--- a/doc-src/TutorialI/Protocol/Message.thy Wed Aug 22 23:23:48 2012 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy Wed Aug 22 23:45:49 2012 +0200
@@ -8,8 +8,9 @@
header{*Theory of Agents and Messages for Security Protocols*}
-theory Message imports Main uses "../../antiquote_setup.ML" begin
-setup {* Antiquote_Setup.setup *}
+theory Message imports Main begin
+ML_file "../../antiquote_setup.ML"
+setup Antiquote_Setup.setup
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"