Re: [isabelle] Isabelle2014-RC0 available for testing

Dear Cornelius,

In Isabelle2013-2, the simproc finite_Collect has taken care of the tuples and solved your goal. In Isabelle2014-RC0, this simproc has been disabled by default because it sometimes complicates proofs or crashes. You can enable the simproc by declaring

  [[simproc add: finite_Collect]]

either globally with "declare" or locally with "using".


On 07/07/14 17:55, C. Diekmann wrote:
I found some problems.

The following can be solved by isabelle 2013-2 but not by Isabelle 2014-RC0:
lemma "finite X ⟹ finite {(x1, x2) ∈ X. P x1 x2}" by simp
In Isabelle 2014-RC0, also try0 and sledgehammer fail.
I suppose it is because of the tuple notation?

When a proof fails, the output buffer displays: "...  method⌂: ...".
Notice the triangle-like symbol. The same strange symbol is displayed
for an ML error.

Finally, when I try to sledgehammer something in one of my thys, the
prover crashes.
"Welcome to Isabelle/HOL (Isabelle2014-RC0: July 2014)
Malformed message:
bad chunk (unexpected EOF after 0 of 7314 bytes)
message_output terminated
line 84: 15324 Segmentation fault      (core dumped) "$POLY" -q -i
$ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/"
"$MLTEXT")" --error-exit < /dev/null

standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 139"
I will try to reproduce this in a minimal example


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