# HG changeset patch
# User wenzelm
# Date 1126018790 -7200
# Node ID 44d8fbc2e52da052c363b13ff050604de86f8dea
# Parent  746bb4c5680071ce2f81f558bc7c1c7f33a4bc7b
axclass: name space prefix is now "c_class" instead of just "c";
typedef: proper support for polymorphic sets;

diff -r 746bb4c56800 -r 44d8fbc2e52d NEWS
--- a/NEWS	Tue Sep 06 16:59:48 2005 +0200
+++ b/NEWS	Tue Sep 06 16:59:50 2005 +0200
@@ -35,7 +35,7 @@
 pattern. Available in ProofGeneral under 'ProofGeneral -> Find
 Theorems' or C-c C-f.  Example:
 
-  C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL."
+  C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL."
 
 prints the last 100 theorems matching the pattern "(_::nat) + _ + _",
 matching the current goal as introduction rule and not having "HOL."
@@ -149,6 +149,11 @@
 is already included here); see also FOL/ex/IffExample.thy;
 INCOMPATIBILITY.
 
+* axclass: name space prefix for class "c" is now "c_class" (was "c"
+before); "cI" is no longer bound, use "c.intro" instead.
+INCOMPATIBILITY.  This change avoids clashes of fact bindings for
+axclasses vs. locales.
+
 * Improved internal renaming of symbolic identifiers -- attach primes
 instead of base 26 numbers.
 
@@ -209,13 +214,13 @@
 * New syntax 'name(i-j, i-, i, ...)' for referring to specific
 selections of theorems in named facts via index ranges.
 
-* More efficient treatment of intermediate checkpoints in interactive
-theory development.
-
 * 'print_theorems': in theory mode, really print the difference
 wrt. the last state (works for interactive theory development only),
 in proof mode print all local facts (cf. 'print_facts');
 
+* More efficient treatment of intermediate checkpoints in interactive
+theory development.
+
 
 *** Locales ***
 
@@ -377,6 +382,9 @@
 removed: r(|x := x r|) = r.  INCOMPATIBILITY: old proofs break
 occasionally, since simplification is more powerful by default.
 
+* typedef: proper support for polymorphic sets, which contain extra
+type-variables in the term.
+
 * Simplifier: automatically reasons about transitivity chains
 involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics
 provided by Provers/trancl.ML as additional solvers.  INCOMPATIBILITY: