# HG changeset patch
# User slotosch
# Date 856196664 -3600
# Node ID f1a6997cdc0654652149f17395930ad7faa91351
# Parent  024654b7591957d02f5dc5f9ed67398a85bd5c30
described changes for HOLCF-Version without rules and arities

diff -r 024654b75919 -r f1a6997cdc06 NEWS
--- a/NEWS	Mon Feb 17 17:23:14 1997 +0100
+++ b/NEWS	Mon Feb 17 17:24:24 1997 +0100
@@ -4,6 +4,15 @@
 
 New in Isabelle94-8 (??????????? 1997 FIXME)
 ---------------------------------------
+* HOLCF changes: derived all rules and arities 
+  + axiomatic type classes instead of classes 
+  + typedef instead of faking type definitions
+  + eliminated the initernal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
+  + new axclasses cpo,chfin,flat with flat<chfin<pcpo<cpo<po
+  + eliminated the types void, one, tr
+  + use unit lift and bool lift (with translations) instead of one and tr
+  + eliminated blift from Lift3.thy (use Def instead of blift)
+  all eliminated rules are derivd as theorems --> no visible changes 
 
 * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss.
 
@@ -61,6 +70,8 @@
 
 * the NEWS file;
 
+Changes in HOLCF:
+
 
 New in Isabelle94-7 (November 96)
 ---------------------------------