# HG changeset patch
# User wenzelm
# Date 1127901014 -7200
# Node ID 6d277e731096af16304fb198a24e3f1de86c5f0b
# Parent 8cc72452695c01f93441698c22fd67c815b1091c
revert 'defs' advertisement;
diff -r 8cc72452695c -r 6d277e731096 ANNOUNCE
--- a/ANNOUNCE Wed Sep 28 11:50:13 2005 +0200
+++ b/ANNOUNCE Wed Sep 28 11:50:14 2005 +0200
@@ -5,7 +5,7 @@
This release provides substantial advances over Isabelle2004, see the
first 1000 lines of NEWS in the distribution for more details. Some
-notable features are:
+highlights are:
* Interpretation of locale expressions in theories, locales, and proof
contexts.
@@ -17,15 +17,12 @@
* General 'find_theorems' command (by term patterns, as
intro/elim/simp rules etc.).
-* Commands for generating adhoc draft documents.
+* Commands for generating ad-hoc draft documents.
* Support for Unicode proof documents (UTF-8).
* Major internal reorganizations and performance improvements.
-* 'defs': more checks for overloading, but less checks for cyclic
-dependencies!
-
You may get Isabelle2005 from the following mirror sites:
diff -r 8cc72452695c -r 6d277e731096 Admin/website/index.html
--- a/Admin/website/index.html Wed Sep 28 11:50:13 2005 +0200
+++ b/Admin/website/index.html Wed Sep 28 11:50:14 2005 +0200
@@ -45,7 +45,7 @@
Now available: Isabelle 2005
- Some notable features:
+ Some highlights:
- Interpretation of locale expressions in theories, locales, and proof contexts.
- Substantial library improvements (HOL, HOL-Complex, HOLCF).
@@ -54,9 +54,6 @@
- Commands for generating adhoc draft documents.
- Support for Unicode proof documents (UTF-8).
- Major internal reorganizations and performance improvements.
- - More well-formedness checks of overloaded
- definitions, but fails to recognize certain ill-formed definitions
- that Isabelle2004 would have rejected outright!
[Cumulative NEWS]