|
4382
|
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)
|