Is there an attribute to hide the display of flex-flex pairs?
Oh dear, what ungodly thing are you doing :D
rewrite... :D 1.jpg
(It doesn't seem to lift schematic variables properly in the context of bound variables.)
What does the "(derive)" do?
Exports the final proof term.
Ah, I saw only know that this is an upper case "Lemma"
I was wondering if you'd somehow overwritten Isabelle's "lemma" command
FYI there does not seem to be a way to disable it at the moment as it is hardwired: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-March/msg00101.html
(Side remark) It would be good if there were some kind of link between here and the mailing list so we wouldn't have to cross post..
There's an open task on phabricator that considers replacing the email list: https://isabelle-dev.sketis.net/T9
Last updated: Dec 07 2023 at 08:19 UTC