[isabelle] Problem with induction_schema
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"
But this leads to looping:
lemma "P 0 â (âx. P x â P (Suc x)) â P x"
Apparently, there is some strange issue with the variable names here.
This archive was generated by a fusion of
Pipermail (Mailman edition) and