[isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE



Hi,

I do this with "Auto Methods" checked in the PIDE options:

theorem
  "(!!P. P::bool) ==> PROP P"
oops

The processes Isabelle2013-2.exe and poly.exe start taking close to 100% of my CPU, and don't give up. The PIDE gets unresponsive, and I have to terminate everthing.

With "Auto Methods" unchecked, I can use "try0" and they go into overdrive, but they slowly shut down over about 10 seconds.

As a side note, I can run Sledgehammer, and the ATPs can be at over 96% of the CPU, but the PIDE never gets unresponsive.

I attach a screen shot.

For anyone interested, here's what I use to look at "Trueprop", which is shown in the screenshot:

notation Trueprop ("_\<Colon>\<^sub>T" [1000] 1000)

Forgetting about brackets, typing, and Trueprop can sometimes result in me expending negative mental energy. Confused neurons, mucking about in the grey matter, too many to count, connecting the most embarrassing of logical dots.

Thanks,
GB

Attachment: 131213_for_all_bool_hangs_pide.png
Description: PNG image



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.