[isabelle-dev] simps_of_case and function types

Lars Hupel hupel at in.tum.de
Tue Aug 25 18:56:26 CEST 2015

Previous message (by thread): [isabelle-dev] simps_of_case and function types
Next message (by thread): [isabelle-dev] State of affairs with simplifier tracing?
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

> Does anyone rely on the more liberal form "... = P (case x of ...)"
> accepted at the moment?

Yes, I do. Sorry :-)

Cheers
Lars

Previous message (by thread): [isabelle-dev] simps_of_case and function types
Next message (by thread): [isabelle-dev] State of affairs with simplifier tracing?
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the isabelle-dev mailing list