diff -r 308ba2488d40 -r e9fd5eff62c1 ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Mon Sep 17 00:07:40 2012 +0100 +++ b/ProgTutorial/Base.thy Thu Oct 04 13:00:31 2012 +0100 @@ -5,9 +5,6 @@ "ML_prf" :: prf_decl and "ML_val" :: diag *) -uses - ("output_tutorial.ML") - ("antiquote_setup.ML") begin notation (latex output) @@ -27,8 +24,8 @@ HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n)) *} -use "output_tutorial.ML" -use "antiquote_setup.ML" +ML_file "output_tutorial.ML" +ML_file "antiquote_setup.ML" setup {* OutputTutorial.setup *} setup {* AntiquoteSetup.setup *}