summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

Admin/BUGS

author | wenzelm |

Fri, 19 Jan 2001 19:26:02 +0100 | |

changeset 10941 | 6c09cae3b4ad |

parent 4382 | c1536da54f52 |

child 10991 | 2e59c831cf07 |

permissions | -rw-r--r-- |

more bugs;

Isabelle BUGS -- history of reported faults =========================================== 1. Symptom: hyp_subst_tac does nothing if the selected equality involves type unknowns. Cause: it uses the simplifier, which ignores such equalities. Fix: check for type unknowns in hypsubst/inspect_pair; change interface function dest_eq to return the type of the equality. (lcp, 5/11/97) 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}"