Re: [isabelle] update_thy
On Wed, 15 Aug 2007, Jeremy Dawson wrote:
> I've just obtained a recent development version of Isabelle, and find that
> update_thy is missing.
This is what the official Isabelle/NEWS file (of the current development
* Theory loader: be more serious about observing the static theory
header specifications (including optional directories), but not the
accidental file locations of previously successful loads. The strict
update policy of former update_thy is now already performed by
use_thy, so the former has been removed; use_thys updates several
theories simultaneously, just as 'imports' within a theory header
specification, but without merging the results. Potential
INCOMPATIBILITY: may need to refine theory headers and commands
ROOT.ML which depend on load order.
Anyway, neither use_thy nor former update_thy should occur in regular
interactive use of Isabelle at all: when processing a theory header
interactively, the system already updates all required theories. Invoking
use_thy (or its simultaneous version use_thys) mostly occurs in batch mode
ROOT.ML files, until we replace these by plain ROOT header specifications
using existing theory syntax.
This archive was generated by a fusion of
Pipermail (Mailman edition) and