[isabelle] type-unsound error



The full text of the sledgehammer error I got is appended here.
Two questions:

1) This error depends on some sorried proofs before it: does this make it uninteresting, or should I submit it anyway? In the first case I will try to complete those proofs (I am positive, though not sure, they can be completed) and see if the error goes away; in the latter case I can save such work.

2) The error message says to report to Isabelle developers, while the official sledgehammer reference explicitly mentions this particular error and says to report to its maintainer:if I do (see 1), whom should I report to?


Thanks,
Marco
PS: possible double post for technical problems, sorry



"remote_e_sine": The prover found a type-unsound proof involving "Domain_converse", "Domain_empty", "Image_empty", "Image_within_domain", "Int_empty_left", "Int_empty_right", "Range_empty", "Set.is_empty_def", "empty_Collect_eq", "empty_iff", "equals0D", "ll1", "ll67", and "mem_Collect_eq" even though a supposedly type-sound encoding was used (or, less likely, your axioms are inconsistent). Please report this to the Isabelle developers.





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