--- a/Admin/BUGS Fri Jan 19 13:35:11 2001 +0100
+++ b/Admin/BUGS Fri Jan 19 19:26:02 2001 +0100
@@ -9,3 +9,33 @@
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)
+
+
+- res_inst_tac bug:
+val [p1, p2] = Goalw [o_def]
+ "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
+by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
+by (res_inst_tac [("h", "%x. @y. (f x::'b) = g y")] p2 1);
+ ^^^^ required!
+Problem: lift_inst_rule only refers to syntactic context of current
+dynamic proof state; old-style goal initially does not contain hyps
+(!!);
+
+Fix: either make assumptions statically scoped (included as hyps in
+goal), or pass additional environment to lift_inst_rule (this would
+improve upon Isar's res_inst_tac as well);
+
+- type infer / inst bug:
+Goal "x = (x::?'a)";
+by (cut_inst_tac [("t", "x")] refl 1);
+
+- bug in prove_goal (!?):
+forall_elim: Variable ?uu has two distinct types
+'a
+'b
+*** The exception above was raised for
+*** (!!uu uua. PROP P (uu, uua)) ==> PROP P xa
+
+- bug in HOL/Set tr':
+term "{x. EX a b c. x = f a b c & P x}"
+prints as: "{f a b c |a b c. P B.0}"