Josh Chen (Mar 23 2020 at 17:15): Josh Chen (Mar 23 2020 at 17:15):Is there an attribute to hide the display of flex-flex pairs?
Manuel Eberl (Mar 23 2020 at 18:05):Oh dear, what ungodly thing are you doing :D
Josh Chen (Mar 23 2020 at 18:08):Debugging rewrite... :D 1.jpg
(It doesn't seem to lift schematic variables properly in the context of bound variables.)
Manuel Eberl (Mar 23 2020 at 18:10):What does the "(derive)" do?
Josh Chen (Mar 23 2020 at 18:11):Exports the final proof term.
Manuel Eberl (Mar 23 2020 at 20:41):Ah, I saw only know that this is an upper case "Lemma"
Manuel Eberl (Mar 23 2020 at 20:41):I was wondering if you'd somehow overwritten Isabelle's "lemma" command
Kevin Kappelmann (Mar 24 2020 at 10:59):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
Josh Chen (Mar 24 2020 at 11:30):(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..
Kevin Kappelmann (Mar 24 2020 at 11:34):There's an open task on phabricator that considers replacing the email list: https://isabelle-dev.sketis.net/T9
Last updated: Apr 26 2024 at 01:06 UTC