Re: [isabelle] Unexpected assumptions in nested contexts



On 13.06.2012 17:02, Lars Hupel wrote:
(!!I. finite I) ==>  ?something_about ?I  [!]

Obviously, this fact says something completely different. Am I doing
something wrong here?

(Also, what does the `[!]` mean after the fact?)

This means that this theorem is not really proven (in most cases this means, that you used "sorry", as you did above).





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