# HG changeset patch
# User wenzelm
# Date 921675282 -3600
# Node ID e9e8af97f48f96b74b8638a30c8a37031dffd618
# Parent  5a6570458d9e181403dd3f308bb3e268d2c9b4c3
HOL/typedef: fixed type inference for representing set;
AxClass.axclass_tac lost the theory argument;

diff -r 5a6570458d9e -r e9e8af97f48f NEWS
--- a/NEWS	Wed Mar 17 13:50:51 1999 +0100
+++ b/NEWS	Wed Mar 17 13:54:42 1999 +0100
@@ -12,6 +12,9 @@
 
 * HOL: the predicate "inj" is now defined by translation to "inj_on";
 
+* HOL/typedef: fixed type inference for representing set; type
+arguments now have to occur explicitly on the rhs as type constraints;
+
 * ZF: The con_defs part of an inductive definition may no longer refer
 to constants declared in the same theory;
 
@@ -73,6 +76,9 @@
 temporal levels more uniformly; introduces INCOMPATIBILITIES due to
 changed syntax and (many) tactics;
 
+* HOL/typedef: fixed type inference for representing set; type
+arguments now have to occur explicitly on the rhs as type constraints;
+
 
 *** ZF ***
 
@@ -99,6 +105,8 @@
 
 *** Internal programming interfaces ***
 
+* AxClass.axclass_tac lost the theory argument;
+
 * tuned current_goals_markers semantics: begin / end goal avoids
 printing empty lines;