# HG changeset patch
# User wenzelm
# Date 1028541651 -7200
# Node ID 3470596f3cd5616cf9d00c3111ce328fdb003bd5
# Parent  f0fdd0499dad3087d4462054af7478c5f88de3f3
updated;

diff -r f0fdd0499dad -r 3470596f3cd5 Admin/BUGS
--- 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
diff -r f0fdd0499dad -r 3470596f3cd5 Admin/CHECKLIST
--- /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$
diff -r f0fdd0499dad -r 3470596f3cd5 Admin/MIRRORS
--- 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 (??)