doc-src/TutorialI/Inductive/Advanced.thy
changeset 48895 4cd4ef1ef4a4
parent 43564 9864182c6bad
--- 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 {*