* Isar/Provers: intro/elim/dest attributes: changed
intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one
should have to change intro!! to intro? only);

--- a/NEWS	Tue Jul 25 00:06:46 2000 +0200
+++ b/NEWS	Tue Jul 25 00:11:38 2000 +0200
@@ -46,7 +46,11 @@
 
 * Isar: changed syntax of local blocks from {{ }} to { };
 
-* Provers: strengthened force_tac by using new first_best_tac
+* Isar/Provers: intro/elim/dest attributes: changed
+intro/intro!/intro!!  flags to intro!/intro/intro? (in most cases, one
+should have to change intro!! to intro? only);
+
+* Provers: strengthened force_tac by using new first_best_tac;
 
 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.
   [| inj ?f;          ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
@@ -90,7 +94,8 @@
 * old-style theories now produce (crude) LaTeX output as well;
 
 * browser info session directories are now self-contained (may be put
-on WWW server seperately);
+on WWW server seperately); improved graphs of nested sessions; removed
+graph for 'all sessions';
 
 
 *** Isar ***
@@ -154,7 +159,9 @@
 
 * names of theorems etc. may be natural numbers as well;
 
-* Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??;
+* Provers: intro/elim/dest attributes: changed intro/intro!/intro!!
+flags to intro!/intro/intro? (in most cases, one should have to change
+intro!! to intro? only);
 
 * 'pr' command: optional goals_limit argument; no longer prints theory
 contexts, but only proof states;