reorganized the main HOL image;
authorwenzelm
Fri Jul 03 17:36:45 1998 +0200 (1998-07-03)
changeset 5125463a0e9df5b5
parent 5124 1ce3cccfacdb
child 5126 01cbf154d926
reorganized the main HOL image;
NEWS
     1.1 --- a/NEWS	Fri Jul 03 17:35:39 1998 +0200
     1.2 +++ b/NEWS	Fri Jul 03 17:36:45 1998 +0200
     1.3 @@ -46,6 +46,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* reorganized the main HOL image: HOL/Integ and String loaded by
     1.8 +default; theory Main includes everything;
     1.9 +
    1.10 +* HOL/Real: a construction of the reals using Dedekind cuts;
    1.11 +
    1.12 +* HOL/record: now includes concrete syntax for record terms (still
    1.13 +lacks important theorems, like surjective pairing and split);
    1.14 +
    1.15  * Inductive definition package: Mutually recursive definitions such as
    1.16  
    1.17    inductive EVEN ODD
    1.18 @@ -60,11 +68,6 @@
    1.19    the recursive sets. Note that the component "mutual_induct" no longer
    1.20    exists - the induction rule is always contained in "induct".
    1.21  
    1.22 -* HOL/Real: a construction of the reals using Dedekind cuts
    1.23 -
    1.24 -* HOL/record: now includes concrete syntax for record terms (still
    1.25 -lacks important theorems, like surjective pairing and split);
    1.26 -
    1.27  * simplification procedure unit_eq_proc rewrites (?x::unit) = (); this
    1.28  is made part of the default simpset of Prod.thy, which COULD MAKE
    1.29  EXISTING PROOFS FAIL (consider 'Delsimprocs [unit_eq_proc];' as last
    1.30 @@ -74,9 +77,9 @@
    1.31  rewriting and classical reasoning (and whatever other tools) similarly
    1.32  to auto_tac, but is aimed to solve the given subgoal totally;
    1.33  
    1.34 -* added option_map_eq_Some to simpset() and claset()
    1.35 +* added option_map_eq_Some to simpset() and claset();
    1.36  
    1.37 -* New directory HOL/UNITY: Chandy and Misra's UNITY formalism
    1.38 +* New directory HOL/UNITY: Chandy and Misra's UNITY formalism;
    1.39  
    1.40  * New theory HOL/Update of function updates:
    1.41    f(a:=b) == %x. if x=a then b else f x