On Wed, 19 Aug 2015, Makarius wrote:
On Wed, 19 Aug 2015, Larry Paulson wrote:
I frequently look at finished theories when looking for useful theorems.
But I’ve noticed a new and undesirable behaviour: I get the message "The
following files are required to resolve theory imports” even thoug
> Does anyone rely on the more liberal form "... = P (case x of ...)"
> accepted at the moment?
Yes, I do. Sorry :-)
Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle
On 25.08.2015 18:16, Lars Noschinski wrote:
> Hi everyone,
> Unfortunately, simps_of_case cannot use the Splitter, as splitter
> applies the split-rule in the wrong direction. So simps_of_case either
> needs to reimplement the Splitter's logic for instantiating the split
> rule or the Splitter need
Hi everyone,
Lars Hupel privately reported a situation where simps_of_case does not
work as expected (refering to 2015 and to 87f0f707a5f8).
I have not solved the issue yet (and will probably not find time the
next two months), so I document my findings here.
fun nosplit where "nosplit x f = (ca
