[isabelle-dev] find_theorems raises UnequalLengths exception
brianh at cs.pdx.edu
Thu Nov 18 17:03:09 CET 2010
Recently I noticed that in HOLCF, whenever I do a theorem search for
theorems containing the constant "UU" (i.e. bottom), the search fails
with an UnequalLengths exception. I tracked the problem down to this
specific theorem from Fun_Cpo.thy: Before this point, find_theorems
"UU" succeeds, and afterward it causes an error.
lemma app_strict: "UU x = UU"
I found that I can also reproduce the problem directly in HOL:
lemma bot_apply: "bot x = bot"
by (simp only: bot_fun_eq)
*** exception UnequalLengths raised
*** At command "find_theorems"
After doing "hg bisect", I traced the origin of the problem:
Can anyone figure this out?
More information about the isabelle-dev