7 Fix: check for type unknowns in hypsubst/inspect_pair; change interface 
7 Fix: check for type unknowns in hypsubst/inspect_pair; change interface 
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 (Messageid: <199710301432.PAA20594@sirius.Informatik.UniBremen.DE> on isabelleusers) 
11 simultaneous instantiations (Messageid: <199710301432.PAA20594@sirius.Informatik.UniBremen.DE> on isabelleusers) 

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; oldstyle 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 

38 

39  bug in HOL/Set tr': 

40 term "{x. EX a b c. x = f a b c & P x}" 

41 prints as: "{f a b c a b c. P B.0}" 