0
$\begingroup$

https://isabelle.systems/cookbook/src/proofs/methods/Chained_Facts.thy

talks about

We note a slight difference. In the variant with intro, a trivial goal remains that we need to solve by ‹assumption›. The reason is that ‹intro› is a ∗‹simple method› in Isabelle jargon, while ‹rule› is ∗‹proper›. Simple methods ignore chained facts and insert them into the goal state, while proper methods will usually act on them in some way.

Is there anything more to know about simple and proper methods? Especially, where can I find a list of the methods belonging to these categories?

Improve this question
$\endgroup$
2
  • $\begingroup$ Is this a reference request? If not, feel free to remove the tag and/or elaborate! $\endgroup$
    – Trebor ♦
    Commented Apr 12, 2023 at 16:50
  • $\begingroup$ I didn't know about that tag but yes, it is! $\endgroup$
    – Gergely
    Commented Apr 13, 2023 at 15:08

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.