Email Gateway (Aug 19 2022 at 17:05): Email Gateway (Aug 19 2022 at 17:05):From: Andrew Gacek <andrew.gacek@gmail.com>
In the Isabelle/HOL tutorial [1] at the top of page 172 the text
refers to "ac_simps" and "ac_simps" as if they mean two different
things. Is this a typo or am I missing something else? For example:
"The name ac_simps refers to the list of all three theorems; similarly
there is ac_simps."
"Simplify using ac_simps and ac_simps."
"apply (simp add: ac_simps ac_simps)"
It looks like some kind of search/replace went wrong perhaps?
-Andrew
[1] http://isabelle.in.tum.de/doc/tutorial.pdf
Email Gateway (Aug 19 2022 at 17:05):From: Tobias Nipkow <nipkow@in.tum.de>
Yes inded, this is the result of a change. In the past we had plus_ac and
times_ac, now we have ac_simps (although the others still exist). The tutorial,
although technically still correct, is not state of the art any longer. Hence we
don't invest much energy when updating it. But thanks for pointing this out, it
would be better to fix it.
Tobias
smime.p7s
Email Gateway (Aug 19 2022 at 17:06):From: Tobias Nipkow <nipkow@in.tum.de>
The first of the tutorials (on the Isabelle pages), "Programming and Proving in
Isabelle/HOL", covers structured proofs and deemphasizes "apply". It is meant as
a compact intro and does not cover everything covered in the old tutorial.
Tobias
smime.p7s
Email Gateway (Aug 19 2022 at 17:06):From: Daniel Horne <d.horne@danielhorne.co.uk>
Is there another tutorial resource that you'd recommend over it?
I've been working through that tutorial, and was previously unaware it was
outdated.
Thanks
Daniel Horne
Last updated: Apr 27 2024 at 01:05 UTC