# HG changeset patch
# User wenzelm
# Date 1126797413 -7200
# Node ID e6f8455c8fcf56b2820356e137f2c14655ccd851
# Parent  551c9a4dd69325051a9fa7eb034045de711055d3
obsolete;

diff -r 551c9a4dd693 -r e6f8455c8fcf Admin/BUGS
--- a/Admin/BUGS	Thu Sep 15 17:16:53 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-
-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)
-