Re: [isabelle] where is "Isabelle/Show me .../Facts" menu in window version of Isabelle



On 27.10.2014 17:53, M A wrote:
> I can not find in plugin or other menu, where can show facts
>  
> show "list.inject" this command can not show facts content.
You should really read the documentation.

You can print lemmas with the "print_statement" or "thm" commands or by
using the find theorems tab of the query panel.
> lemma "P ∧ Q ==> P"
> sledgehammer learn_isar
> sledgehammer [prover = e, fact_filter = mesh, verbose] 
>  
> "mesh": Including 1000 relevant facts: list.inject ...
Do not use fact_filter, verbose and learn_isar. At this point in your
Isabelle career, they won't help you.




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