HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
authorwenzelm
Thu Dec 27 16:43:56 2001 +0100 (2001-12-27)
changeset 1259714822e4436bf
parent 12596 34265656f0b4
child 12598 fa556d3fe5f2
HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
NEWS
     1.1 --- a/NEWS	Tue Dec 25 10:02:20 2001 +0100
     1.2 +++ b/NEWS	Thu Dec 27 16:43:56 2001 +0100
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -239,11 +240,15 @@
     1.9  for ML tools): const "()" renamed "Product_Type.Unity", type "unit"
    1.10  renamed "Product_Type.unit";
    1.11  
    1.12 -* HOL/GroupTheory: group theory examples including Sylow's theorem, by
    1.13 -Florian Kammüller;
    1.14 -
    1.15  * HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
    1.16  
    1.17 +* HOL/GroupTheory: group theory examples including Sylow's theorem (by
    1.18 +Florian Kammüller);
    1.19 +
    1.20 +* HOL/IMP: updated and converted to new-style theory; several parts
    1.21 +turned into readable document, with proper Isar proof texts and some
    1.22 +explanations (by Gerwin Klein);
    1.23 +
    1.24  
    1.25  *** HOLCF ***
    1.26  
    1.27 @@ -251,6 +256,8 @@
    1.28  potential INCOMPATIBILITY; now use plain induct_tac instead of former
    1.29  lift.induct_tac, always use UU instead of Undef;
    1.30  
    1.31 +* HOLCF/IMP: updated and converted to new-style theory;
    1.32 +
    1.33  
    1.34  *** ZF ***
    1.35  
    1.36 @@ -319,6 +326,9 @@
    1.37  * system: Proof General keywords specification is now part of the
    1.38  Isabelle distribution (see etc/isar-keywords.el);
    1.39  
    1.40 +* system: some support for persistent Proof General sessions (refrain
    1.41 +from outdating all loaded theories on startup);
    1.42 +
    1.43  * system: smart selection of Isabelle process versus Isabelle
    1.44  interface, accommodates case-insensitive file systems (e.g. HFS+); may
    1.45  run both "isabelle" and "Isabelle" even if file names are badly