Re: [isabelle] Simple problem with variable instantiation
The variable must be exactly the same as it appears in the theorem, i.e.
?c2.0 and not
All these theorems can be proved automatically by eg. arith.
c fe wrote:
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