Re: [isabelle-dev] Towards the release

2016-01-01 Thread Manuel Eberl 
I still have a few thousand lines of stuff to merge into the 
distribution, most notably the definition of the radius of convergence 
of a series and a number of convergence tests.


This would be nice to have in the distribution because two results of 
mathematical importance rest upon it: the Gamma function and the 
Generalised Binomial Theorem.


The work itself is already, all that remains is to merge it into the 
distribution. I put the files in this repository if anyone wants to look 
at them: https://github.com/3of8/isabelle_summation


The only files that require any real merging (as opposed to just copying 
the file into the distribution) are Summation.thy, 
Extended_Real_Lemma_Bucket.thy, and Liminf_Limsup_Lemma_Bucket.thy. The 
file "Concave.thy" is not required by the rest and does not need to be 
merged.



None of this really has to end up in Isabelle2016; I can also wait for 
the next release. My plan was to meet with Johannes and Fabian after the 
holidays and ask them for their opinions on this material.



Cheers,

Manuel


On 01/01/16 20:24, Makarius wrote:

Isabelle2016-RC0 is published, but we are still in normal incremental
change mode on the isabelle-dev repository.

This is also an opportunity to check NEWS, ANNOUNCE, CONTRIBUTORS, and
the website.


Are there bigger changes still in the pipeline?  Larry are you finished
with the ports from HOL Light, as far as Isabelle2016 is concerned?

Depending on that, the fork point for the release will be a bit sooner
or later.  Lets say in about 2 weeks. Hopefully, Oracle manages to
deliver the next Java 8 update in 3 weeks, as scheduled.


 Makarius
___
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] NEWS: print mode ASCII vs. xsymbols

2016-01-01 Thread Makarius 

On Tue, 29 Dec 2015, Makarius wrote:


This refers to Isabelle/0a5dd617a88c.  A bit more changes may follow later.


Here is an updated summary according to Isabelle2016-RC0, with further 
notes at the bottom:



*** General ***

* Former "xsymbols" syntax with Isabelle symbols is used by default,
  without any special print mode. Important ASCII replacement syntax
  remains available under print mode "ASCII", but less important syntax
  has been removed (see below).

* Support for more arrow symbols, with rendering in LaTeX and Isabelle
  fonts: \ \ \
  \ \ \


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

* Additional abbreviations for syntactic completion may be specified in
  $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with
  support for simple templates using ASCII 007 (bell) as placeholder.


*** Document preparation ***

* HTML presentation uses the standard IsabelleText font and Unicode
  rendering of Isabelle symbols like Isabelle/Scala/jEdit.  The former
  print mode "HTML" loses its special meaning.


*** HOL ***

* Some old and rarely used ASCII replacement syntax has been removed.
  INCOMPATIBILITY, standard syntax with symbols should be used instead.
  The subsequent commands help to reproduce the old forms, e.g. to
  simplify porting old theories:

  notation iff  (infixr "<->" 25)

  notation Times  (infixr "<*>" 80)

  type_notation Map.map  (infixr "~=>" 0)
  notation Map.map_comp  (infixl "o'_m" 55)

  type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)

  notation FuncSet.funcset  (infixr "->" 60)
  notation FuncSet.extensional_funcset  (infixr "->\<^sub>E" 60)

  notation Omega_Words_Fun.conc (infixr "conc" 65)

  notation Preorder.equiv ("op ~~")
and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)

  notation (in topological_space) tendsto (infixr "--->" 55)
  notation (in topological_space) LIMSEQ ("((_)/ > (_))" [60, 60] 60)
  notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)

  notation NSA.approx (infixl "@=" 50)
  notation NSLIMSEQ ("((_)/ NS> (_))" [60, 60] 60)
  notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)

* The alternative notation "\" for type and sort constraints has
  been removed: in LaTeX document output it looks the same as "::".
  INCOMPATIBILITY, use plain "::" instead.

* Library/Monad_Syntax: notation uses symbols \ and \.
  INCOMPATIBILITY.



Note that the IsabelleText font provides new glyphs for \ \ 
\ \ \ \ 
\ \ by stretching official 
code-point descriptions (literally) very far.


With standard Unicode fonts, these may look bad, or just show up as black 
or white box.  We are privileged to live in a space of infinitely many 
Isabelle symbols.


The following resources might be generally interesting to explore 
possibilities in LaTeX:


  http://mirrors.ctan.org/info/symbols/comprehensive/symbols-a4.pdf
  http://detexify.kirelabs.org
  http://milde.users.sourceforge.net/LUCR/Math


Makarius

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

Re: [isabelle-dev] Towards the release

2016-01-01 Thread Makarius 

On Fri, 1 Jan 2016, Lawrence Paulson wrote:

I'm still working on a major theorem. It would be nice to include it if 
possible.


Do you have a time estimate for that?


Makarius

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

Re: [isabelle-dev] Towards the release

2016-01-01 Thread Lawrence Paulson 
I'm still working on a major theorem. It would be nice to include it if 
possible. However, I have no major changes on the order of the real vs of_nat 
rationalisation.
Larry

> On 1 Jan 2016, at 19:24, Makarius  wrote:
> 
> Isabelle2016-RC0 is published, but we are still in normal incremental change 
> mode on the isabelle-dev repository.
> 
> This is also an opportunity to check NEWS, ANNOUNCE, CONTRIBUTORS, and the 
> website.
> 
> 
> Are there bigger changes still in the pipeline?  Larry are you finished with 
> the ports from HOL Light, as far as Isabelle2016 is concerned?
> 
> Depending on that, the fork point for the release will be a bit sooner or 
> later.  Lets say in about 2 weeks. Hopefully, Oracle manages to deliver the 
> next Java 8 update in 3 weeks, as scheduled.
> 
> 
>   Makarius
> ___
> 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