Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

2016-08-08 Thread Makarius
On 08/08/16 17:09, Andreas Lochbihler wrote: > > Additionally, you could declare bundles > with the existing notation > > "(f has_integral x) s" > > for both of them (like is nowadays done for the Lifting package syntax). > Then, you can locally include the notation for the desired integral

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

2016-08-08 Thread Andreas Lochbihler
Hi Johannes, You could define the syntax for has_integral to be literally "(f Bochner.has_integral x) s" and similarly for the other. Additionally, you could declare bundles with the existing notation "(f has_integral x) s" for both of them (like is nowadays done for the Lifting

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

2016-08-08 Thread Johannes Hölzl
Am Montag, den 08.08.2016, 15:03 +0100 schrieb Lawrence Paulson: > Thank you for making this change! > > > > > My idea would be to rename both integrals into something like: > >   has_bc_integral, bc_integrable, bc_integral, > >   has_hk_integral, hk_integrable, hk_integral > > and consequently

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

2016-08-08 Thread Lawrence Paulson
Thank you for making this change! > My idea would be to rename both integrals into something like: > has_bc_integral, bc_integrable, bc_integral, > has_hk_integral, hk_integrable, hk_integral > and consequently rename the integral theorems. I would greatly prefer renaming the relevant

[isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

2016-08-08 Thread Johannes Hölzl
* Renamed session HOL-Multivariate_Analysis to HOL-Analysis. * Moved measure theory from HOL-Probability to HOL-Analysis. When importing HOL-Analysis some theorems need additional name spaces prefixes due to name clashes. INCOMPATIBILITY. The incompatibility is obviously due to the renaming,

Re: [isabelle-dev] [isabelle] Proposal: An update to Multiset theory

2016-08-08 Thread Bertram Felgenhauer
Florian Haftmann wrote: > Hi Bertram, > > > How shall we proceed? As I hinted at earlier I do not have (nor want, at > > this point) push access, but I can prepare a patch or clone of the repo, > > if that helps, or just provide a plain theory file that works with the > > development version of

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

2016-08-08 Thread Lars Hupel
> With a chart showing performance parameters (CPU time, elapsed time, > heap size) in the past few weeks, it should be normally easy to see a > small step or spike for HOL-Proofs or its applications. Happy to assist with that. In a previous mail you indicated that these parameters can be found

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

2016-08-08 Thread Makarius
On 08/08/16 11:14, Lars Hupel wrote: > Dear all, > > the latest build failure for the repository is spurious: > > *** exception Fail raised (line 83 of "./basis/PolyMLException.sml"): > Insufficient memory > > This happened in HOL-Proofs. Makarius, it may or may not be connected to > the recent

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

2016-08-08 Thread Makarius
On 08/08/16 13:13, Manuel Eberl wrote: > I've heard of negative thermal expansion in some materials, but I don't > think RAM is subject to it. (scnr) > > In a more serious fashion: I don't see how ambient temperature could > affect memory usage. I've run into "insufficient memory" and stack >

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

2016-08-08 Thread Tobias Nipkow
On 08/08/2016 13:13, Manuel Eberl wrote: I've heard of negative thermal expansion in some materials, but I don't think RAM is subject to it. (scnr) In a more serious fashion: I don't see how ambient temperature could affect memory usage. I've run into "insufficient memory" and stack overflow

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

2016-08-08 Thread Manuel Eberl
I've heard of negative thermal expansion in some materials, but I don't think RAM is subject to it. (scnr) In a more serious fashion: I don't see how ambient temperature could affect memory usage. I've run into "insufficient memory" and stack overflow problems in Isabelle several times

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

2016-08-08 Thread Makarius
On 08/08/16 11:14, Lars Hupel wrote: > the latest build failure for the repository is spurious: > > *** exception Fail raised (line 83 of "./basis/PolyMLException.sml"): > Insufficient memory > > This happened in HOL-Proofs. I have tried Isabelle/1e7c5bbea36d once again with

Re: [isabelle-dev] NEWS: proof outline with cases

2016-08-08 Thread Andreas Lochbihler
Hi Makarius, Just a quick feedback on the proof outlines: they are great! But sometimes quotes are needed around the case name (e.g., if it is a keyword like "try" or "oracle", or if it is a case of an induction rule by the function package for an equation which has been split up by the