[isabelle] Problem with induction_schema



Hallo,

Simon and I just came across the following problem with induction_schema which is present both in Isabelle2015 and 45eee631ea4f:

This works as intended:
lemma "P 0 â (ân. P n â P (Suc n)) â P x"
  apply (induction_schema)

But this leads to looping:

lemma "P 0 â (âx. P x â P (Suc x)) â P x"
  apply (induction_schema)


Apparently, there is some strange issue with the variable names here.

Manuel




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