> 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
*** 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
*** 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
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
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 /
