Admin/BUGS
author berghofe
Mon Feb 03 11:44:23 2003 +0100 (2003-02-03)
changeset 13803 84cb1ff80f25
parent 13447 3470596f3cd5
permissions -rw-r--r--
Fill in version information in lib/Tools/version.
paulson@4382
     1
paulson@4382
     2
Isabelle BUGS -- history of reported faults
paulson@4382
     3
===========================================
paulson@4382
     4
paulson@4382
     5
1.  Symptom: hyp_subst_tac does nothing if the selected equality involves type
paulson@4382
     6
    unknowns.  Cause: it uses the simplifier, which ignores such equalities.
paulson@4382
     7
    Fix: check for type unknowns in hypsubst/inspect_pair;  change interface
paulson@4382
     8
    function dest_eq to return the type of the equality. (lcp, 5/11/97)
paulson@4382
     9
paulson@4382
    10
2.  Symptom: read_instantiate_sg has problems instantiating types in some
paulson@4382
    11
    simultaneous instantiations (Message-id: <199710301432.PAA20594@sirius.Informatik.Uni-Bremen.DE> on isabelle-users)
wenzelm@10941
    12