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 
snapshot) says:

* 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 MHonArc.