Re: [isabelle] Pending sort hypotheses


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 !

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