Admin/BUGS
author wenzelm
Fri Oct 12 12:05:46 2001 +0200 (2001-10-12)
changeset 11724 f727aa96ae2e
parent 10991 2e59c831cf07
child 13447 3470596f3cd5
permissions -rw-r--r--
declare impE iffD1 iffD2 as elim of Pure;
     1 
     2 Isabelle BUGS -- history of reported faults
     3 ===========================================
     4 
     5 1.  Symptom: hyp_subst_tac does nothing if the selected equality involves type
     6     unknowns.  Cause: it uses the simplifier, which ignores such equalities.
     7     Fix: check for type unknowns in hypsubst/inspect_pair;  change interface
     8     function dest_eq to return the type of the equality. (lcp, 5/11/97)
     9 
    10 2.  Symptom: read_instantiate_sg has problems instantiating types in some
    11     simultaneous instantiations (Message-id: <199710301432.PAA20594@sirius.Informatik.Uni-Bremen.DE> on isabelle-users)
    12 
    13 
    14 - res_inst_tac bug:
    15 val [p1, p2] = Goalw [o_def]
    16      "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
    17 by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
    18 by (res_inst_tac [("h", "%x. @y. (f x::'b) = g y")] p2 1);
    19                                       ^^^^ required!
    20 Problem: lift_inst_rule only refers to syntactic context of current
    21 dynamic proof state; old-style goal initially does not contain hyps
    22 (!!);
    23 
    24 Fix: either make assumptions statically scoped (included as hyps in
    25 goal), or pass additional environment to lift_inst_rule (this would
    26 improve upon Isar's res_inst_tac as well);
    27 
    28 - type infer / inst bug:
    29 Goal "x = (x::?'a)";
    30 by (cut_inst_tac [("t", "x")] refl 1);
    31 
    32 - bug in prove_goal (!?):
    33 forall_elim: Variable ?uu has two distinct types
    34 'a
    35 'b
    36 *** The exception above was raised for
    37 *** (!!uu uua. PROP P (uu, uua)) ==> PROP P xa