[isabelle] Simple problem with variable instantiation


I stumbled upon a problem with Isabelle 2007 that didn't occur in
Isabelle 2003 (IIRC). I made a small (not very meaningful) example:

lemma test:
"c1 + (c2::nat) < a ==> c1 < a"
apply simp

lemma test':
"a + (b::nat) < c ==> a < c"
apply simp

lemma test2:
"7 < (a::nat) ==> 5 < a"
(* Now use either [1] or [2] *)
[1] apply (rule_tac "c2.0"="2" in test)
[2] apply (rule_tac b=2 in test')
apply simp

If I want to use test to proof test2 I can't instantiate c2.
That isn't a big problem as I can just make lemmas like test' but if
there is a simple solution to this I'd be interested to hear about it.

Christoph Feller

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.