Admin/BUGS
author nipkow
Wed Aug 04 11:25:08 2004 +0200 (2004-08-04)
changeset 15106 e8cef6993701
parent 13447 3470596f3cd5
permissions -rw-r--r--
aded comment
     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)
    12