Email Gateway (Aug 18 2022 at 17:05): Email Gateway (Aug 18 2022 at 17:05):From: li yongjian <lyj238@gmail.com>
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
Email Gateway (Aug 18 2022 at 17:05):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: Nov 21 2024 at 12:39 UTC