[isabelle] metis



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.