Thank you for this, Florian. The one thing I had hoped for when I initiated
this change was that one can write n-1 just like n+1, but that doesn't
quite work yet, probably because you have some special syntax for what used to
be negative numerals. This may ease the conversion, but can we get rid
Hi René and Florian (and other experts in code generation),
I move this thread from users to dev because it is now getting into detailed discussions
and commit ids.
I've moved my setup for String.literal from Containers to the distribution and pushed the
changes to testboard), but I realised
On Mon, 18 Nov 2013, Jasmin Christian Blanchette wrote:
A question that arises is whether we should have only datatype_new
(and primrec_new; i.e. the LFP part) in HOL or also codatatype
(and primcorec; i.e. the GFP part). The BNF package is organized in
such a way that it can be split in the
Hi Makarius,
Am 20.11.2013 um 14:12 schrieb Makarius makar...@sketis.net:
Dmitriy had sent me some explanations which sessions represent the material
to be moved to HOL in either case, but I never tried it out myself. It is
high time to do that now. In particularly I would like to get a
We have a bad state in Isabelle/d983a020489d:
* HOL-BNF_Example fails like this:
*** Theory loader: failed to load Gram_Lang (unresolved DTree)
*** Theory loader: failed to load Parallel (unresolved DTree)
*** Extra variables on rhs: dtree_unfold
*** The error(s) above occurred in definition:
On 20.11.2013 17:17, Makarius wrote:
Looking at http://isabelle.in.tum.de/reports/Isabelle/ is odd: spinning
wheel for 4bc48d713602 (time comment 8 hours ago).
So maybe mira is down or non-terminating.
In the last days, the CouchDB seems to be down more often than not.
Maybe next week I'll
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
Open text buffers take precedence over copies within the file-system.
This refers to Isabelle/05738b7d8191.
It is only the first half of it: PIDE document model, without document
Am 20.11.2013 um 17:17 schrieb Makarius makar...@sketis.net:
We have a bad state in Isabelle/d983a020489d:
* HOL-BNF_Example fails like this:
*** Theory loader: failed to load Gram_Lang (unresolved DTree)
*** Theory loader: failed to load Parallel (unresolved DTree)
*** Extra variables
We have a problem with Isabelle2013-1 that cannot be ignored. A changeset
is included for information.
Are there any side-conditions on the timing of a follow-up Isabelle2013-2,
e.g. concerning AFP which needs to be updated once more?
I am basically ready to ship a new release within a few
On Wed, 20 Nov 2013, Makarius wrote:
Are there any side-conditions on the timing of a follow-up
Isabelle2013-2, e.g. concerning AFP which needs to be updated once more?
I am basically ready to ship a new release within a few days +/-. To
make it not too odd, we could wait until the start of
If there will already be a new release, would it perhaps be possible to
merge the fix (given there is a robust one) for this 'adhoc_overloading
raises TYPE' issue [1] ?
This error is quite puzzling. And it occurs even if one does not know
what the packages 'adhoc_overloading' and 'coercions' are
11 matches
Mail list logo
