equal
deleted
inserted
replaced
8 function dest_eq to return the type of the equality. (lcp, 5/11/97) |
8 function dest_eq to return the type of the equality. (lcp, 5/11/97) |
9 |
9 |
10 2. Symptom: read_instantiate_sg has problems instantiating types in some |
10 2. Symptom: read_instantiate_sg has problems instantiating types in some |
11 simultaneous instantiations (Message-id: <199710301432.PAA20594@sirius.Informatik.Uni-Bremen.DE> on isabelle-users) |
11 simultaneous instantiations (Message-id: <199710301432.PAA20594@sirius.Informatik.Uni-Bremen.DE> on isabelle-users) |
12 |
12 |
13 |
|
14 - res_inst_tac bug: |
|
15 val [p1, p2] = Goalw [o_def] |
|
16 "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P"; |
|
17 by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1); |
|
18 by (res_inst_tac [("h", "%x. @y. (f x::'b) = g y")] p2 1); |
|
19 ^^^^ required! |
|
20 Problem: lift_inst_rule only refers to syntactic context of current |
|
21 dynamic proof state; old-style goal initially does not contain hyps |
|
22 (!!); |
|
23 |
|
24 Fix: either make assumptions statically scoped (included as hyps in |
|
25 goal), or pass additional environment to lift_inst_rule (this would |
|
26 improve upon Isar's res_inst_tac as well); |
|
27 |
|
28 - type infer / inst bug: |
|
29 Goal "x = (x::?'a)"; |
|
30 by (cut_inst_tac [("t", "x")] refl 1); |
|
31 |
|
32 - bug in prove_goal (!?): |
|
33 forall_elim: Variable ?uu has two distinct types |
|
34 'a |
|
35 'b |
|
36 *** The exception above was raised for |
|
37 *** (!!uu uua. PROP P (uu, uua)) ==> PROP P xa |
|