[isabelle-dev] Frag / Poly_Mapping
Attached is a port of the HOL Light “frag” library (free Abelian groups) built upon Poly_Mapping. It’s a mess, especially with the combination of frag and Poly_Mapping names. Some of it clearly could be added to Poly_Mapping, maybe all of it. But it needs to be rationalised. Comments / advice? Larry Frag.thy Description: Binary data ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] function (default) is legacy feature (since 2010)
Are there any remaining uses of "function (default)"? changeset: 41417:211dbd42f95d parent: 41414:00b2b6716ed8 user:krauss date:Wed Dec 29 21:52:41 2010 +0100 function (default) is legacy feature I don't see any remaining applications in Isabelle + AFP. So it looks like we can just remove it without further ado. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: discontinued old-style goal cases
*** Isar *** * Implicit cases goal1, goal2, goal3, etc. have been discontinued (legacy feature since Isabelle2016). This refers to 8c240fdeffcb. The NEWS for Isabelle2016 already explain that the proof method "goal_cases" is the proper way to do it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: discontinued old-style inner comments
*** General *** * Old-style inner comments (* ... *) within the term language are no longer supported (legacy feature in Isabelle2018). This refers to Isabelle/6e9df530b441. There were a few remaining uses in AFP. Notable changes are AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources generated by LEM (!). I don't know how LEM is maintained: it needs to produce different inner comments next time, and can actually use \ CARTOUCHE notation uniformly for inner and outer comments -- also note that this needs to be LaTeX-conformant, e.g. by another nested cartouche or \<^verbatim>CARTOUCHE. Now that (* ... *) is no longer part of the term language, Tobias can finish the infix syntax update project, to get rid of the slightly odd extra spaces for infixes with *. There is also a chance that this will speed up the inner parser and/or grammar updates, which happen quite often (e.g. for local syntax). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] function (default) is legacy feature (since 2010)
> On 24 Sep 2018, at 6:23 am, Makarius wrote: > > Are there any remaining uses of "function (default)"? > > changeset: 41417:211dbd42f95d > parent: 41414:00b2b6716ed8 > user:krauss > date:Wed Dec 29 21:52:41 2010 +0100 > function (default) is legacy feature > > > I don't see any remaining applications in Isabelle + AFP. So it looks > like we can just remove it without further ado. Confirming that this would also be safe from our side. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: discontinued old-style inner comments
> There were a few remaining uses in AFP. Notable changes are > AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources > generated by LEM (!). I don't know how LEM is maintained: it needs to > produce different inner comments next time, and can actually use > \ CARTOUCHE notation uniformly for inner and outer comments -- > also note that this needs to be LaTeX-conformant, e.g. by another nested > cartouche or \<^verbatim>CARTOUCHE. The way this works is that I'll have to send them a patch. This should hopefully be simple enough. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
