[isabelle-dev] find_theorems raises UnequalLengths exception

[Lawrence Paulson]

That is certainly my change, but I don't understand why preventing self-referential type instantiations should affect the find_theorems function. Can you get a full trace back from the exception? 

Larry

On 18 Nov 2010, at 16:03, Brian Huffman wrote:

> Hello everyone,
> 
> 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:
> 
> theory Scratch
> imports Orderings
> begin
> 
> find_theorems "bot"
> 
> lemma bot_apply: "bot x = bot"
> by (simp only: bot_fun_eq)
> 
> find_theorems "bot"
> 
> *** exception UnequalLengths raised
> *** At command "find_theorems"
> 
> After doing "hg bisect", I traced the origin of the problem:
> 
> http://isabelle.in.tum.de/repos/isabelle/rev/b654fa27fbc4
> 
> Can anyone figure this out?
> 
> - Brian
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev