[isabelle-dev] lemma addition
noschinl at in.tum.de
Thu Aug 1 22:01:21 CEST 2013
On 01.08.2013 17:19, Makarius wrote:
>> Both of which are discharged by blast. If we look at the theorems
>> blast uses to prove
>> ⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B
>> (how this can be done is described in Section 3.7 of the Isabelle
>> Cookbook), we see that Relation.converse_iff plays a role, which was
>> declared with the iff attribute.
> I did not understand this mysterious reference. Which version of the
> Cookbook, which page exactly?
It is less mysterious than other references on this list...
Section 3.7, p. 66ff in  gives recipes how proof terms can be
inspected. It is what worked best for me for getting ideas of blast proofs.
`> Using only canonical information reveals these possibilities that might
> be little known:
> * print_options: blast_trace, blast_stats, but this looks a bit chatty
> and of limited practical use
They seem to be mostly useful for debugging blast itself.
More information about the isabelle-dev