updated;
authorwenzelm
Mon Aug 05 12:00:51 2002 +0200 (2002-08-05 ago)
changeset 134473470596f3cd5
parent 13446 f0fdd0499dad
child 13448 3196f93030bb
updated;
Admin/BUGS
Admin/CHECKLIST
Admin/MIRRORS
     1.1 --- a/Admin/BUGS	Fri Aug 02 21:40:47 2002 +0200
     1.2 +++ b/Admin/BUGS	Mon Aug 05 12:00:51 2002 +0200
     1.3 @@ -10,28 +10,3 @@
     1.4  2.  Symptom: read_instantiate_sg has problems instantiating types in some
     1.5      simultaneous instantiations (Message-id: <199710301432.PAA20594@sirius.Informatik.Uni-Bremen.DE> on isabelle-users)
     1.6  
     1.7 -
     1.8 -- res_inst_tac bug:
     1.9 -val [p1, p2] = Goalw [o_def]
    1.10 -     "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
    1.11 -by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
    1.12 -by (res_inst_tac [("h", "%x. @y. (f x::'b) = g y")] p2 1);
    1.13 -                                      ^^^^ required!
    1.14 -Problem: lift_inst_rule only refers to syntactic context of current
    1.15 -dynamic proof state; old-style goal initially does not contain hyps
    1.16 -(!!);
    1.17 -
    1.18 -Fix: either make assumptions statically scoped (included as hyps in
    1.19 -goal), or pass additional environment to lift_inst_rule (this would
    1.20 -improve upon Isar's res_inst_tac as well);
    1.21 -
    1.22 -- type infer / inst bug:
    1.23 -Goal "x = (x::?'a)";
    1.24 -by (cut_inst_tac [("t", "x")] refl 1);
    1.25 -
    1.26 -- bug in prove_goal (!?):
    1.27 -forall_elim: Variable ?uu has two distinct types
    1.28 -'a
    1.29 -'b
    1.30 -*** The exception above was raised for
    1.31 -*** (!!uu uua. PROP P (uu, uua)) ==> PROP P xa
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/Admin/CHECKLIST	Mon Aug 05 12:00:51 2002 +0200
     2.3 @@ -0,0 +1,27 @@
     2.4 +
     2.5 +Checklist for official releases
     2.6 +===============================
     2.7 +
     2.8 +- make sure that etc/isar-keywords.el and etc/isar-keywords-ZF.el are
     2.9 +up-to-date; in ML use ``ProofGeneral.write_keywords ""'' and
    2.10 +``ProofGeneral.write_keywords "ZF"'';
    2.11 +
    2.12 +- check ANNOUNCE, README, INSTALL, NEWS, Admin/page;
    2.13 +
    2.14 +- run tests with *all* supported ML systems (yes this is tedious!);
    2.15 +
    2.16 +- maintain Docs:
    2.17 +    Doc/Contents
    2.18 +    Distribution/doc/Contents
    2.19 +    Admin/index.html
    2.20 +
    2.21 +- maintain Logics:
    2.22 +    Admin/makedist
    2.23 +    Distribution/build
    2.24 +    Distribution/lib/Tools/makeall
    2.25 +    Distribution/lib/html/index1.html
    2.26 +    Distribution/lib/html/index2.html
    2.27 +    Doc/Logics/intro.tex
    2.28 +    Doc/Logics/logics.tex
    2.29 +
    2.30 +$Id$
     3.1 --- a/Admin/MIRRORS	Fri Aug 02 21:40:47 2002 +0200
     3.2 +++ b/Admin/MIRRORS	Mon Aug 05 12:00:51 2002 +0200
     3.3 @@ -8,7 +8,3 @@
     3.4  * New Jersey (USA)
     3.5  http://ftp.research.bell-labs.com/dist/smlnj/isabelle/source.html
     3.6  Dave MacQueen <dbm@research.bell-labs.com>
     3.7 -
     3.8 -* Stanford (USA) (??)
     3.9 -ftp://rodin.stanford.edu/pub/smlnj/isabelle/source.html
    3.10 -Lal George (??)