Re: [isabelle] Metalogical "spec" not resolved automatically



Nicole Rauch wrote:

1. !! N. [| 0 < N; P N |] ==> P (Suc 0)
2. !! N. [| 0 < N; P N; 0 < M |] ==> P M

The meta-forall ranges over the whole expression:

!! N. ( [| 0 < N; P N |] ==> P (Suc 0) )

So the statements are not provable.

Alex





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