[isabelle] Failing simproc



Hi *,

I stumbled upon some funny behaviour which prevents the simplifier in proving "True" in Isabelle2012 (also in 8a1ef12f7e6d). The reduced example is attached.

Dmitriy
theory Simproc_Fail
imports Main
begin

notepad
begin
  have "(\<And>ys zs. length ys < Suc (length zs + length ys))" by simp
  hence True apply simp sorry
end

end


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