Re: [isabelle] metis



Virtually every call to metis has been generated automatically, using sledgehammer. Read the appropriate documentation on sledgehammer. It is easy, as no configuration is required.

Larry Paulson


On 22 Feb 2011, at 08:07, li yongjian wrote:

> Hi, dear all:
>  Recently I read proof scripts in HOL/probablity.
>  I find many proof commands on metis, for example,
>        by(metis Diff_empty compl_sets...)
> 
> The command metis is new for me, althogh I have tried to find some document
> on it, but
> it is diffculty for me to learn to use it. For instance,
>  In the above code,
>  I can guess some parameters of theorems used such as compl_sets if I use
> the metis command ,  but I cannot find all.  Therefore it is diffcult for me
> to use it.
> 
> Are there more documents on metis, especially on how to use it eficiently in
> Isabelle.
> 
> lyj






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