NEWS
changeset 24172 06e42cf7df4e
parent 24110 4ab3084e311c
child 24187 8bdf5ca5871f
     1.1 --- a/NEWS	Tue Aug 07 17:01:35 2007 +0200
     1.2 +++ b/NEWS	Tue Aug 07 20:19:48 2007 +0200
     1.3 @@ -26,8 +26,13 @@
     1.4  
     1.5  * Theory loader: be more serious about observing the static theory
     1.6  header specifications (including optional directories), but not the
     1.7 -accidental file locations of previously successful loads.  Potential
     1.8 -INCOMPATIBILITY, may need to refine theory headers.
     1.9 +accidental file locations of previously successful loads.  The strict
    1.10 +update policy of former update_thy is now already performed by
    1.11 +use_thy, so the former has been removed; use_thys updates several
    1.12 +theories simultaneously, just as 'imports' within a theory header
    1.13 +specification, but without merging the results.  Potential
    1.14 +INCOMPATIBILITY: may need to refine theory headers and commands
    1.15 +ROOT.ML which depend on load order.
    1.16  
    1.17  * Theory loader: optional support for content-based file
    1.18  identification, instead of the traditional scheme of full physical
    1.19 @@ -172,6 +177,19 @@
    1.20  very easy to avoid global references, which would not observe Isar
    1.21  toplevel undo/redo and fail to work with multithreading.
    1.22  
    1.23 +Various global ML references of Pure and HOL have been turned into
    1.24 +configuration options:
    1.25 +
    1.26 +  Unify.search_bound		unify_search_bound
    1.27 +  Unify.trace_bound		unify_trace_bound
    1.28 +  Unify.trace_simp		unify_trace_simp
    1.29 +  Unify.trace_types		unify_trace_types
    1.30 +  Simplifier.simp_depth_limit	simp_depth_limit
    1.31 +  Blast.depth_limit		blast_depth_limit
    1.32 +  DatatypeProp.dtK		datatype_distinctness_limit
    1.33 +  fast_arith_neq_limit  	fast_arith_neq_limit
    1.34 +  fast_arith_split_limit	fast_arith_split_limit
    1.35 +
    1.36  * Named collections of theorems may be easily installed as context
    1.37  data using the functor NamedThmsFun (see
    1.38  src/Pure/Tools/named_thms.ML).  The user may add or delete facts via