equal
deleted
inserted
replaced
|
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) |