Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] writing a proof method after "qed"


view this post on Zulip Email Gateway (Oct 28 2020 at 09:55):

From: Lawrence Paulson <lp15@cam.ac.uk>
Is there a less ugly to express this?

qed (use in ‹fastforce+›)

Omitting the “use in” yields an error message: Undefined method: "cartouche"

Larry

view this post on Zulip Email Gateway (Oct 28 2020 at 10:05):

From: Jakub Kądziołka <kuba@kadziolka.net>
I might be missing something, but the following syntax, without any
cartouche, seems to work for me:

qed fastforce+

Regards,
Jakub Kądziołka

view this post on Zulip Email Gateway (Oct 28 2020 at 10:52):

From: Lawrence Paulson <lp15@cam.ac.uk>
I guess I simplified it too much. But is there something similar for

qed (force simp: add_ac+)

?

Larry

view this post on Zulip Email Gateway (Oct 28 2020 at 10:54):

From: Manuel Eberl <eberlm@in.tum.de>
What about

qed (force simp: add_ac)+

Manuel


Last updated: Jul 15 2022 at 23:21 UTC