[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,

  Viktor

theory TypeSpec = Main:
typedecl obj

lemma works:
"[| ALL n1 n2. k n1 = k n2 --> n1 = n2;
     k x1 = k x2 |] ==> x1 = x2"
apply auto
done

lemma fails:
"[| ALL n1 n2. (k :: obj => obj) n1 = (k :: obj => obj) n2 --> n1 = n2;
     k (x1::obj) = k (x2::obj) |] ==> (x1::obj) = (x2::obj)"
apply auto
sorry

end





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