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