# HG changeset patch
# User wenzelm
# Date 1345671949 -7200
# Node ID 4cd4ef1ef4a4a503dc554708ea8f8fe8f5667c28
# Parent  e794efa84045cfb5e7d821d0d71c6bc664535e59
prefer ML_file over old uses;
updated generated files;

diff -r e794efa84045 -r 4cd4ef1ef4a4 doc-src/IsarImplementation/Thy/document/Base.tex
--- 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
diff -r e794efa84045 -r 4cd4ef1ef4a4 doc-src/System/Thy/document/Base.tex
--- 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}%
 %
diff -r e794efa84045 -r 4cd4ef1ef4a4 doc-src/TutorialI/Inductive/Advanced.thy
--- 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 {*
diff -r e794efa84045 -r 4cd4ef1ef4a4 doc-src/TutorialI/Inductive/Even.thy
--- 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 *}
diff -r e794efa84045 -r 4cd4ef1ef4a4 doc-src/TutorialI/Protocol/Message.thy
--- 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"