--- a/NEWS Mon Sep 10 12:00:28 2012 +0200
+++ b/NEWS Mon Sep 10 12:13:39 2012 +0200
@@ -9,6 +9,12 @@
* Command 'ML_file' evaluates ML text from a file directly within the
theory, without any predeclaration via 'uses' in the theory header.
+* Old command 'use' command and corresponding keyword 'uses' in the
+theory header are legacy features and will be discontinued soon.
+Tools that load their additional source files may imitate the
+'ML_file' implementation, such that the system can take care of
+dependencies properly.
+
* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which
is called fastforce / fast_force_tac already since Isabelle2011-1.
--- a/src/Doc/IsarRef/Spec.thy Mon Sep 10 12:00:28 2012 +0200
+++ b/src/Doc/IsarRef/Spec.thy Mon Sep 10 12:13:39 2012 +0200
@@ -51,13 +51,11 @@
admissible.
@{rail "
- @@{command theory} @{syntax name} imports \\ keywords? uses? @'begin'
+ @@{command theory} @{syntax name} imports keywords? \\ @'begin'
;
imports: @'imports' (@{syntax name} +)
;
keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and')
- ;
- uses: @'uses' ((@{syntax name} | @{syntax parname}) +)
"}
\begin{description}
@@ -84,14 +82,6 @@
with and without proof, respectively. Additional @{syntax tags}
provide defaults for document preparation (\secref{sec:tags}).
- The optional @{keyword_def "uses"} specification declares additional
- dependencies on external files (notably ML sources). Files will be
- loaded immediately (as ML), unless the name is parenthesized. The
- latter case records a dependency that needs to be resolved later in
- the text, usually via explicit @{command_ref "use"} for ML files;
- other file formats require specific load commands defined by the
- corresponding tools or packages.
-
\item @{command (global) "end"} concludes the current theory
definition. Note that some other commands, e.g.\ local theory
targets @{command locale} or @{command class} may involve a