Admin/BUGS

changeset 10941 | 6c09cae3b4ad |

parent 4382 | c1536da54f52 |

child 10991 | 2e59c831cf07 |

--- a/Admin/BUGS Fri Jan 19 13:35:11 2001 +0100 +++ b/Admin/BUGS Fri Jan 19 19:26:02 2001 +0100 @@ -9,3 +9,33 @@ 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 + +- bug in HOL/Set tr': +term "{x. EX a b c. x = f a b c & P x}" +prints as: "{f a b c |a b c. P B.0}"