Admin/BUGS
author webertj
Fri, 26 Mar 2004 12:21:50 +0100
changeset 14487 157d0ea7b2da
parent 13447 3470596f3cd5
permissions -rw-r--r--
Installed solvers now determined at call time (as opposed to compile time)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4382
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     1
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     2
Isabelle BUGS -- history of reported faults
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     3
===========================================
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     4
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     5
1.  Symptom: hyp_subst_tac does nothing if the selected equality involves type
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     6
    unknowns.  Cause: it uses the simplifier, which ignores such equalities.
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     7
    Fix: check for type unknowns in hypsubst/inspect_pair;  change interface
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     8
    function dest_eq to return the type of the equality. (lcp, 5/11/97)
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
     9
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
    10
2.  Symptom: read_instantiate_sg has problems instantiating types in some
c1536da54f52 Comprehensive (??) list of bugs, fixed or not
paulson
parents:
diff changeset
    11
    simultaneous instantiations (Message-id: <199710301432.PAA20594@sirius.Informatik.Uni-Bremen.DE> on isabelle-users)
10941
6c09cae3b4ad more bugs;
wenzelm
parents: 4382
diff changeset
    12