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

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

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

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

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

* 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

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

> 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

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

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

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

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

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

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