# Re: [isabelle] Pending sort hypotheses

*To*: cl-isabelle-users at lists.cam.ac.uk
*Subject*: Re: [isabelle] Pending sort hypotheses
*From*: Henri.Debrat at loria.fr
*Date*: Wed, 4 Jul 2012 15:08:02 +0200
*In-reply-to*: <mailman.59106.1341402876.29855.cl-isabelle-users@lists.cam.ac.uk>
*References*: <mailman.59106.1341402876.29855.cl-isabelle-users@lists.cam.ac.uk>

Hi,
Thanks a lot for all your previous explanations.
Now, let's try some really dummy test.
lemma univbool_a: "UNIV = { True, False }" by auto
(* this is nothing but the standard UNIV_bool theorem *)
lemma univbool_b: "UNIV = { False, True }" by auto
lemma test_a: "False" using univbool_a finite_UNIV
by (blast dest:emeasure_point_measure_finite)
lemma test_b: "False" using univbool_b finite_UNIV
by (blast dest:emeasure_point_measure_finite)
The proof of test_a ends with the usual sort_contraint error, while test_b just makes the CPU go mad. I just cannot understand what is happening here !
H.

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