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
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
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
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
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
> 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
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
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
>
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
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
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
* 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,
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
13 matches
Mail list logo
