summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 17275 | 44d8fbc2e52d |

parent 17269 | c5a52602c4a7 |

child 17371 | 923ef4a8c672 |

--- 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: