Hi all, Am 12.09.2018 um 11:12 schrieb Lawrence Paulson: > I regard it as indispensable. But it does need better pretty printing. > Also I greatly prefer the if/for format to assume/fix.
Am 12.09.2018 um 12:12 schrieb Mathias Fleury: > I have my own version of explore > (https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy), which > does not have better pretty printing, but has two variants that I find > indispensable: explore_have produces "have … if … for …" > and explore_lemma produces "lemma fixes … assumes … shows …". There is > even an option for cartouches. proper pretty printing should not be to difficult; maybe Sledgehammer_Isar_Proof can be reused or a common base extracted from that. explore_have should maybe just be the standard variant. I would suggest a further variant explore <method expr> would actually be the same as apply <method expr> but, given a proof goal ‹!!ys. Qs ==> D›, for remaining goals ‹!!xs1. Ps1 ==> C1› … ‹!!xsn. Psn ==> Cn› after method application suggest a proof skeleton proof - fix ys assume Qs have C1 if Ps1 for xs1 moreover have C2 if Ps2 for xs2 … moreover have Cn if Psn for xsn ultimately show D by qed <method expr> and hence provide a way to quickly get to the essence of a proof after initial »explore auto«. Cheers, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
