Re: [isabelle-dev] [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main

2017-03-03 Thread Lawrence Paulson 
As I understand it, the star notation is the standard way of denoting the 
injection of an entity from, say, the standard reals to the non-standard reals. 
It is normally written as a prefix operator. Maybe we could do something using 
our  ⋆ character. But we have two other naming conventions in NSA: the prefixes 
hr and NS. 

A lot of work needs to be done in order to bring this development up-to-date. 
I’m glad to see that the star operator is now fully integrated into the 
axiomatic type class system, but quite a lot of material made redundant by that 
step is still present.

Larry

> On 3 Mar 2017, at 09:28, Makarius  wrote:
> 
> On 27/02/17 18:22, Lawrence Paulson wrote:
>> 
>> Note: I have no suggestions for improving the star notation of
>> non-standard analysis, mentioned in the last paragraph.
> 
> Can you point to some literature or papers that use the notation in a
> canonical form?
> 
> 
>   Makarius
> 
> 

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

Re: [isabelle-dev] Build failure in slow sessions

2017-03-03 Thread Makarius 
On 24/02/17 14:24, Makarius wrote:
> On 22/02/17 10:14, Lars Hupel wrote:
>>
>> 11:07:25.458 Iptables_Semantics_Examples: theory
>> Analyze_Synology_Diskstation
>> 19:01:48.518 Run out of store - interrupting threads
>>
>> So, nothing happens for a while and then we get an out of memory error.
>> Note that the "slow" sessions are executed on 64 bit with an abundance
>> of memory.
> 
> More now I have switched back to Poly/ML 5.6 (18f3d341f8c0), until I
> find time to look what is really going on there.

See also
http://lists.inf.ed.ac.uk/pipermail/polyml/2017-February/001978.html
http://lists.inf.ed.ac.uk/pipermail/polyml/2017-February/001980.html
http://lists.inf.ed.ac.uk/pipermail/polyml/2017-March/001981.html

The conclusion of this thread is that we skip Poly/ML 5.7 and David
Matthews looks again later.


Makarius

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

Re: [isabelle-dev] [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main

2017-03-03 Thread Makarius 
On 27/02/17 18:22, Lawrence Paulson wrote:
> 
> Note: I have no suggestions for improving the star notation of
> non-standard analysis, mentioned in the last paragraph.

Can you point to some literature or papers that use the notation in a
canonical form?


Makarius


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