NEWS
changeset 53656 a3c5ff796d84
parent 53615 f557a4645f61
child 53681 7e80b558c751
equal deleted inserted replaced
53648:924579729403 53656:a3c5ff796d84
   125   - Refined table of Isabelle symbol abbreviations (see
   125   - Refined table of Isabelle symbol abbreviations (see
   126     $ISABELLE_HOME/etc/symbols).
   126     $ISABELLE_HOME/etc/symbols).
   127 
   127 
   128 
   128 
   129 *** Pure ***
   129 *** Pure ***
       
   130 
       
   131 * Former global reference trace_unify_fail is now available as
       
   132 configuration option "unify_trace_failure" (global context only).
   130 
   133 
   131 * Type theory is now immutable, without any special treatment of
   134 * Type theory is now immutable, without any special treatment of
   132 drafts or linear updates (which could lead to "stale theory" errors in
   135 drafts or linear updates (which could lead to "stale theory" errors in
   133 the past).  Discontinued obsolete operations like Theory.copy,
   136 the past).  Discontinued obsolete operations like Theory.copy,
   134 Theory.checkpoint, and the auxiliary type theory_ref.  Minor
   137 Theory.checkpoint, and the auxiliary type theory_ref.  Minor