* HOL/Library: a collection of generic theories to be used together
authorwenzelm
Wed Oct 18 23:24:39 2000 +0200 (2000-10-18)
changeset 1024587771e2f49fe
parent 10244 61824cf550db
child 10246 d8c968e6329a
* HOL/Library: a collection of generic theories to be used together
with main HOL; the theory loader path already includes this directory
by default; the following existing theories have been moved here:
HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
(as While_Combinator);
NEWS
     1.1 --- a/NEWS	Wed Oct 18 17:47:01 2000 +0200
     1.2 +++ b/NEWS	Wed Oct 18 23:24:39 2000 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -6,6 +7,22 @@
     1.9  * HOL: induct renamed to lfp_induct;
    1.10  
    1.11  
    1.12 +*** Document preparation ***
    1.13 +
    1.14 +* improved isabelle style files; more abstract symbol implementation
    1.15 +(should now use \isamath{...} and \isatext{...} in custom symbol
    1.16 +definitions);
    1.17 +
    1.18 +
    1.19 +*** HOL ***
    1.20 +
    1.21 +* HOL/Library: a collection of generic theories to be used together
    1.22 +with main HOL; the theory loader path already includes this directory
    1.23 +by default; the following existing theories have been moved here:
    1.24 +HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
    1.25 +(as While_Combinator);
    1.26 +
    1.27 +
    1.28  New in Isabelle99-1 (October 2000)
    1.29  ----------------------------------
    1.30