# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1349352031 -3600 # Node ID e9fd5eff62c1bb3a684044619e9a76b90a02e75f # Parent 308ba2488d401cd25e10f2d2208887c08a8f16dd removed "use" for "ML_file" 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 *} diff -r 308ba2488d40 -r e9fd5eff62c1 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Mon Sep 17 00:07:40 2012 +0100 +++ b/ProgTutorial/First_Steps.thy Thu Oct 04 13:00:31 2012 +0100 @@ -72,43 +72,21 @@ However, both commands will only play minor roles in this tutorial (we most of the time make sure that the ML-code is defined outside proofs). - - - + Once a portion of code is relatively stable, you usually want to export it to a separate ML-file. Such files can then be included somewhere inside a - theory by using the command \isacommand{use}. For example + theory by using the command \isacommand{ML\_file}. For example \begin{quote} \begin{tabular}{@ {}l} \isacommand{theory} First\_Steps\\ \isacommand{imports} Main\\ - \isacommand{uses}~@{text "(\"file_to_be_included.ML\")"} @{text "\<dots>"}\\ \isacommand{begin}\\ \ldots\\ - \isacommand{use}~@{text "\"file_to_be_included.ML\""}\\ + \isacommand{ML\_file}~@{text "\"file_to_be_included.ML\""}\\ \ldots \end{tabular} \end{quote} - - The \isacommand{uses}-command in the header of the theory is needed in order - to indicate the dependency of the theory on the ML-file. Alternatively, the - file can be included by just writing in the header - - \begin{quote} - \begin{tabular}{@ {}l} - \isacommand{theory} First\_Steps\\ - \isacommand{imports} Main\\ - \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\ - \isacommand{begin}\\ - \ldots - \end{tabular} - \end{quote} - - Note that no parentheses are given in this case. Note also that the included - ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle - is unable to record all file dependencies, which is a nuisance if you have - to track down errors. *} section {* Printing and Debugging\label{sec:printing} *} diff -r 308ba2488d40 -r e9fd5eff62c1 ProgTutorial/Package/Simple_Inductive_Package.thy --- a/ProgTutorial/Package/Simple_Inductive_Package.thy Mon Sep 17 00:07:40 2012 +0100 +++ b/ProgTutorial/Package/Simple_Inductive_Package.thy Thu Oct 04 13:00:31 2012 +0100 @@ -1,9 +1,10 @@ theory Simple_Inductive_Package imports Main "../Base" keywords "simple_inductive" :: thy_decl -uses "simple_inductive_package.ML" begin +ML_file "simple_inductive_package.ML" + (* simple_inductive trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" diff -r 308ba2488d40 -r e9fd5eff62c1 ProgTutorial/Recipes/Oracle.thy --- a/ProgTutorial/Recipes/Oracle.thy Mon Sep 17 00:07:40 2012 +0100 +++ b/ProgTutorial/Recipes/Oracle.thy Thu Oct 04 13:00:31 2012 +0100 @@ -1,6 +1,5 @@ theory Oracle imports "../Appendix" -uses ("external_solver.ML") begin section {* Writing an Oracle (TBD)\label{rec:oracle} *} @@ -32,7 +31,7 @@ ``external solver'': *} -use "external_solver.ML" +ML_file "external_solver.ML" text {* We do, however, know that the solver provides a function diff -r 308ba2488d40 -r e9fd5eff62c1 progtutorial.pdf Binary file progtutorial.pdf has changed