Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Admin/BUGS
author wenzelm
Thu, 14 Jul 2005 19:28:39 +0200
changeset 16854 fdd362b7e980
parent 13447 3470596f3cd5
permissions -rw-r--r--
removed itlist, rev_itlist -- use fold_rev, fold instead; improved end_itlist;


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