[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:
"c1 + (c2::nat) < a ==> c1 < a"
"a + (b::nat) < c ==> a < c"
"7 < (a::nat) ==> 5 < a"
(* Now use either  or  *)
 apply (rule_tac "c2.0"="2" in test)
 apply (rule_tac b=2 in test')
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and