[isabelle-dev] NEWS: Indentation according to Isabelle outer syntax

[Makarius]

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Indentation according to Isabelle outer syntax, cf. action
"indent-lines" (shortcut C+i).


This refers to Isabelle/52349e41d5dc.

It is only the second round of refinement, beyond direct imitation of
the old proof-indent.el from Proof General (see Isabelle/005b490f0ce2).

There might be odd combinations that still need to be ironed out -- Isar
in 2016 is more complex than in 1999.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] {0::nat..<n} = {..<n}

[Florian Haftmann]

> The whole setup has grown over time and initially I may have preferred
> {.. 
> I agree, sums look nicer with {.. {0.. otherwise implicit in the type.
> 
> Tobias
> 
> On 04/07/2016 21:00, Florian Haftmann wrote:
>>> The problem with {..>> every lemma involving {m..>> {..>> all problems: not all proof methods invoke simp all the time.
>>>
>>> I consider {..>> gains very little by using it. One could even think aout replacing it by
>>> {0..>
>> OK, then {0..> realize before, rules concerning {0..> to state as rules concerning {..> bound.
>>
>> However then I suggest to add a few lemmas to emphasize that decision,
>> e.g.
>>
>> lemma lessThan_atLeast0:
>>   fixes n :: nat
>>   shows "{..>   by (simp add: atLeast0LessThan)
>>
>> lemma atMost_atLeast0:
>>   fixes n :: nat
>>   shows "{..n} = {0..n}"
>>   by (simp add: atLeast0AtMost)
>>
>> Currently, only their symmetrics are present, but not these, which would
>> suggest that {..>
>> Similarly for ‹{0..> {..n}›
>>
>> What remains a little bit unsatisfactory is the printing of sums and
>> products:
>>
>> term "setsum (\n. n ^ 3) {0..> 0..
>> term "setsum (\n. n ^ 3) {.. 3\
>> term "setsum (\n. n ^ 3) {0..m::nat}" -- \\n = 0..m.
>> n ^ 3\
>> term "setsum (\n. n ^ 3) {..m::nat}" -- \\n\m. n
>> ^ 3\
>>
>> Here the non-canonical forms are superior to read, but I think we can
>> live with that.
>>
>> Since I have currently laid hands-on on that matter, I would offer to
>> add lessThan_atLeast0, atMost_atLeast0 and ‹{0..> {0..n}› to the distribution.  I would also polish one or two definitions
>> in Binomial.thy which currently involve the non-canonical forms.
>>
>> Maybe lessThan_atLeast0 and atMost_atLeast0 are suitable candidates for
>> default simp rules also then.
>>
>> Cheers,
>> Florian
>>
 obviously on natural numbers ‹{0.. 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

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

Re: [isabelle-dev] Considered harmful: surj

[Florian Haftmann]

> Yes I second that. It surely is a good idea to just use it only as a
> input translation.

See now 6af79184bef3.

Florian

> 
>  - Johannes
> 
> Am Samstag, den 02.07.2016, 21:08 +0200 schrieb Florian Haftmann:
>> Hi all,
>>  
>> since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f =
>> UNIV›. This is a little bit unfortunate since an ordinary equation is
>> just hidden in output that way, resulting in lots of casual
>> confusion. I
>> would suggest to turn ‹surj› into a mere input abbreviation, similar
>> to
>> ‹trivial_limit› which also covers an equality. This may also open the
>> possibility to re-introduce ‹surj_on f A› as in input abbreviation
>> for
>> ‹range f = A›, which got abolished in cf26dd7395e4, leaving a strange
>> assymmetry wrt. inj(_on), bij(_betw).
>>  
>> Cheers,
>>  Florian
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
>> le-dev
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

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

Re: [isabelle-dev] Build NEWS

[Lars Hupel]

>> I’m sure there are quite some papers which reference the /devel
>> entries.
> 
> I should hope not - they make no sense to cite, because their whole
> purpose is to change on a daily basis.

I'm with Gerwin here. In fact, the devel pages clearly state: "Please
refer to release versions only in citations."

If you need to refer to some current development for any purposes, you
should really be using the Mercurial id, just as we do for the Isabelle
repository.

Cheers
Lars.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Build NEWS

[Andreas Lochbihler]

For published versions, there probably should not be any /devel-entries links. But for 
papers under submission, people may have updated their AFP entries and want the reviewers 
to access the updated material. At least that is what I used to do for many ITP 
submissions. So it might be good to keep the /devel-entries URLs alive at least for some 
transition period.


Andreas

On 11/07/16 08:09, Gerwin Klein wrote:

On 11 Jul 2016, at 16:03, Johannes Hölzl  wrote:


Am Sonntag, den 10.07.2016, 22:37 +0200 schrieb Lars Hupel:

Dear AFP developers,

some of you may have noticed that the "AFP devel" pages have not been
updated since April. This is partly my fault because I migrated the
infrastructure and partly not my fault because the scripts to produce
these pages make a lot of assumptions about the infrastructure :-)

Anyway, there's now a reboot of these pages available at:

   

Note that this is a preview: The status is still [skipped] everywhere
and most download links don't work. This will be fixed some time this
week.

As soon as that's done, the old links ("/devel-entries" and the like)
will go offline.


Can't we just let the /devel-entries redirect to http://devel. ?


That would not be too hard, but



I’m sure there are quite some papers which reference the /devel entries.


I should hope not - they make no sense to cite, because their whole purpose is 
to change on a daily basis.

Cheers,
Gerwin



The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Build NEWS

[Gerwin Klein]

On 11 Jul 2016, at 16:03, Johannes Hölzl  wrote:
>
> Am Sonntag, den 10.07.2016, 22:37 +0200 schrieb Lars Hupel:
>> Dear AFP developers,
>>
>> some of you may have noticed that the "AFP devel" pages have not been
>> updated since April. This is partly my fault because I migrated the
>> infrastructure and partly not my fault because the scripts to produce
>> these pages make a lot of assumptions about the infrastructure :-)
>>
>> Anyway, there's now a reboot of these pages available at:
>>
>>   
>>
>> Note that this is a preview: The status is still [skipped] everywhere
>> and most download links don't work. This will be fixed some time this
>> week.
>>
>> As soon as that's done, the old links ("/devel-entries" and the like)
>> will go offline.
>
> Can't we just let the /devel-entries redirect to http://devel. ?

That would not be too hard, but


> I’m sure there are quite some papers which reference the /devel entries.

I should hope not - they make no sense to cite, because their whole purpose is 
to change on a daily basis.

Cheers,
Gerwin



The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Build NEWS

[Johannes Hölzl]

Am Sonntag, den 10.07.2016, 22:37 +0200 schrieb Lars Hupel:
> Dear AFP developers,
> 
> some of you may have noticed that the "AFP devel" pages have not been
> updated since April. This is partly my fault because I migrated the
> infrastructure and partly not my fault because the scripts to produce
> these pages make a lot of assumptions about the infrastructure :-)
> 
> Anyway, there's now a reboot of these pages available at:
> 
>   
> 
> Note that this is a preview: The status is still [skipped] everywhere
> and most download links don't work. This will be fixed some time this
> week.
> 
> As soon as that's done, the old links ("/devel-entries" and the like)
> will go offline.

Can't we just let the /devel-entries redirect to http://devel. ?  I'm
sure there are quite some papers which reference the /devel entries.

> Cheers
> Lars

 - Johannes
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev