I’d be in favour!
Larry
> On 23 Feb 2019, at 15:07, Makarius wrote:
>
> It might be better to introduce a proof-local version of 'abbreviation'.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On 23/02/2019 11:45, Lars Hupel wrote:
>> After a lot of refinements by David Matthews we are moving towards the
>> new Poly/ML 5.8 release. Isabelle/8c587dd44f51 already bundles a Poly/ML
>> version of that number, without being official yet. The Isabelle NEWS
>> already talk about an official
On 23/02/2019 12:25, Lawrence Paulson wrote:
> Which reminds me: I define such abbreviations all the time, using “let”.
> Could let-abbreviations be folded upon printing?
>
>> On 23 Feb 2019, at 09:10, Manuel Eberl wrote:
>>
>> I for one almost always do
>>
>> define G where "G =
Which reminds me: I define such abbreviations all the time, using “let”. Could
let-abbreviations be folded upon printing?
Larry
> On 23 Feb 2019, at 09:10, Manuel Eberl wrote:
>
> I for one almost always do
>
> define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"
>
> in
After a lot of refinements by David Matthews we are moving towards the
new Poly/ML 5.8 release. Isabelle/8c587dd44f51 already bundles a
Poly/ML
version of that number, without being official yet. The Isabelle NEWS
already talk about an official release:
Is it intentional that the system
I for one almost always do
define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"
in such cases, perhaps occasionally combined with a
note [simp] = G_def [symmetric]
at least during the "exploratory" stage of Isar proof writing.
Without that, statements and proof obligations
