[isabelle] Type annotations
I have two simple lemmas whose proof requires instantiating a universal
quantifier. Could anyone tell me why the first one works and the second
one does not? The first one can be obtained from the first one by
stripping all type annotations. Thanks,
theory TypeSpec = Main:
"[| ALL n1 n2. k n1 = k n2 --> n1 = n2;
k x1 = k x2 |] ==> x1 = x2"
"[| ALL n1 n2. (k :: obj => obj) n1 = (k :: obj => obj) n2 --> n1 = n2;
k (x1::obj) = k (x2::obj) |] ==> (x1::obj) = (x2::obj)"
This archive was generated by a fusion of
Pipermail (Mailman edition) and