Admin/BUGS

adapted to new PureThy.add_thms etc.;

+
−
+
−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: <[e-mail]> on isabelle-users)