# HG changeset patch
# User wenzelm
# Date 899480205 -7200
# Node ID 463a0e9df5b5f20351ff233f7adeab9aa694445b
# Parent  1ce3cccfacdb508c74a2bd7715dafdc4bbb1e276
reorganized the main HOL image;

diff -r 1ce3cccfacdb -r 463a0e9df5b5 NEWS
--- a/NEWS	Fri Jul 03 17:35:39 1998 +0200
+++ b/NEWS	Fri Jul 03 17:36:45 1998 +0200
@@ -46,6 +46,14 @@
 
 *** HOL ***
 
+* reorganized the main HOL image: HOL/Integ and String loaded by
+default; theory Main includes everything;
+
+* HOL/Real: a construction of the reals using Dedekind cuts;
+
+* HOL/record: now includes concrete syntax for record terms (still
+lacks important theorems, like surjective pairing and split);
+
 * Inductive definition package: Mutually recursive definitions such as
 
   inductive EVEN ODD
@@ -60,11 +68,6 @@
   the recursive sets. Note that the component "mutual_induct" no longer
   exists - the induction rule is always contained in "induct".
 
-* HOL/Real: a construction of the reals using Dedekind cuts
-
-* HOL/record: now includes concrete syntax for record terms (still
-lacks important theorems, like surjective pairing and split);
-
 * simplification procedure unit_eq_proc rewrites (?x::unit) = (); this
 is made part of the default simpset of Prod.thy, which COULD MAKE
 EXISTING PROOFS FAIL (consider 'Delsimprocs [unit_eq_proc];' as last
@@ -74,9 +77,9 @@
 rewriting and classical reasoning (and whatever other tools) similarly
 to auto_tac, but is aimed to solve the given subgoal totally;
 
-* added option_map_eq_Some to simpset() and claset()
+* added option_map_eq_Some to simpset() and claset();
 
-* New directory HOL/UNITY: Chandy and Misra's UNITY formalism
+* New directory HOL/UNITY: Chandy and Misra's UNITY formalism;
 
 * New theory HOL/Update of function updates:
   f(a:=b) == %x. if x=a then b else f x