On Thu, 27 Jun 2013, Makarius wrote:
This is a continuation of the following threads from some weeks ago:
[isabelle-dev] auto raises a TYPE exception
Here is the updated example from that thread for Isabelle/a3b175675843:
consts P :: 'a set = bool
lemma P_Int [intro]: P A == P B == P (A
On Thu, 27 Jun 2013, Makarius wrote:
This is a continuation of the following threads from some weeks ago:
[isabelle] SELECT_GOAL and schematic variables
In Isabelle/a3b175675843 the examples from that thread now work without
surprises (even after shifting indexes erratically):
inductive
For sure, nested function variables like P (B x) are much too risky to use with
automation. It's essential, at the very least, to ensure that P is some
definite abstraction.
Larry
On 27 Jun 2013, at 12:00, Makarius makar...@sketis.net wrote:
On Thu, 27 Jun 2013, Makarius wrote:
This is a
