--- a/Admin/BUGS Fri Aug 02 21:40:47 2002 +0200
+++ b/Admin/BUGS Mon Aug 05 12:00:51 2002 +0200
@@ -10,28 +10,3 @@
2. Symptom: read_instantiate_sg has problems instantiating types in some
simultaneous instantiations (Message-id: <199710301432.PAA20594@sirius.Informatik.Uni-Bremen.DE> on isabelle-users)
-
-- res_inst_tac bug:
-val [p1, p2] = Goalw [o_def]
- "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
-by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
-by (res_inst_tac [("h", "%x. @y. (f x::'b) = g y")] p2 1);
- ^^^^ required!
-Problem: lift_inst_rule only refers to syntactic context of current
-dynamic proof state; old-style goal initially does not contain hyps
-(!!);
-
-Fix: either make assumptions statically scoped (included as hyps in
-goal), or pass additional environment to lift_inst_rule (this would
-improve upon Isar's res_inst_tac as well);
-
-- type infer / inst bug:
-Goal "x = (x::?'a)";
-by (cut_inst_tac [("t", "x")] refl 1);
-
-- bug in prove_goal (!?):
-forall_elim: Variable ?uu has two distinct types
-'a
-'b
-*** The exception above was raised for
-*** (!!uu uua. PROP P (uu, uua)) ==> PROP P xa
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/CHECKLIST Mon Aug 05 12:00:51 2002 +0200
@@ -0,0 +1,27 @@
+
+Checklist for official releases
+===============================
+
+- make sure that etc/isar-keywords.el and etc/isar-keywords-ZF.el are
+up-to-date; in ML use ``ProofGeneral.write_keywords ""'' and
+``ProofGeneral.write_keywords "ZF"'';
+
+- check ANNOUNCE, README, INSTALL, NEWS, Admin/page;
+
+- run tests with *all* supported ML systems (yes this is tedious!);
+
+- maintain Docs:
+ Doc/Contents
+ Distribution/doc/Contents
+ Admin/index.html
+
+- maintain Logics:
+ Admin/makedist
+ Distribution/build
+ Distribution/lib/Tools/makeall
+ Distribution/lib/html/index1.html
+ Distribution/lib/html/index2.html
+ Doc/Logics/intro.tex
+ Doc/Logics/logics.tex
+
+$Id$
--- a/Admin/MIRRORS Fri Aug 02 21:40:47 2002 +0200
+++ b/Admin/MIRRORS Mon Aug 05 12:00:51 2002 +0200
@@ -8,7 +8,3 @@
* New Jersey (USA)
http://ftp.research.bell-labs.com/dist/smlnj/isabelle/source.html
Dave MacQueen <dbm@research.bell-labs.com>
-
-* Stanford (USA) (??)
-ftp://rodin.stanford.edu/pub/smlnj/isabelle/source.html
-Lal George (??)