Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
* HOL: the class of all HOL types is now called "type" rather than
authorwenzelm
Sat, 01 Dec 2001 18:50:41 +0100
changeset 12335 db4d5f498742
parent 12334 60bf75e157e4
child 12336 2d4561866642
* HOL: the class of all HOL types is now called "type" rather than "term"; INCOMPATIBILITY, need to adapt references to this type class in axclass/classes, instance/arities, and (usually rare) occurrences in typings (of consts etc.); internally the class is called "HOL.type", ML programs should refer to HOLogic.typeS;
NEWS file | annotate | diff | comparison | revisions 
--- a/NEWS	Fri Nov 30 17:55:13 2001 +0100
+++ b/NEWS	Sat Dec 01 18:50:41 2001 +0100
@@ -158,6 +158,12 @@
 
   - remove all special provisions on numerals in proofs;
 
+* HOL: the class of all HOL types is now called "type" rather than
+"term"; INCOMPATIBILITY, need to adapt references to this type class
+in axclass/classes, instance/arities, and (usually rare) occurrences
+in typings (of consts etc.); internally the class is called
+"HOL.type", ML programs should refer to HOLogic.typeS;
+
 * HOL/record package improvements:
   - new derived operations "fields" to build a partial record section,
     "extend" to promote a fixed record to a record scheme, and
isabelle