Admin/BUGS
changeset 10941 6c09cae3b4ad
parent 4382 c1536da54f52
child 10991 2e59c831cf07
equal deleted inserted replaced
10940:02900bff1cfb 10941:6c09cae3b4ad
     7     Fix: check for type unknowns in hypsubst/inspect_pair;  change interface
     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)
     8     function dest_eq to return the type of the equality. (lcp, 5/11/97)
     9 
     9 
    10 2.  Symptom: read_instantiate_sg has problems instantiating types in some
    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)
    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
       
    38 
       
    39 - bug in HOL/Set tr':
       
    40 term "{x. EX a b c. x = f a b c & P x}"
       
    41 prints as: "{f a b c |a b c. P B.0}"