Hi Florian,
I have been quite busy the last few days and hence did find the time
to answer you email quickly.
> This however breaks Quickcheck/Narrowing where the lazy nature of
> pattern bindings has been exploited, may be unconsciously. A minimal
> example is attached
On 05/30/2013 05:32 PM, Makarius wrote:
On Thu, 30 May 2013, Lukas Bulwahn wrote:
I was thinking of a ML antiquotation for check_property @{context}
and I was thinking of @{spec ...} and some context flags that lets
spec either only compile, or check with values.
This should allow
On 12/11/2012 10:27 PM, Makarius wrote:
On Mon, 10 Dec 2012, Makarius wrote:
On Fri, 30 Nov 2012, Lukas Bulwahn wrote:
It must be considered unmaintained. The benchmarks themself I will
irregularly have time on weekends and nights to have a look, but I
cannot keep up with Isabelle roaring
On 11/29/2012 10:22 PM, Makarius wrote:
On Thu, 29 Nov 2012, Makarius wrote:
I've also started some bisection about where the problem comes from,
without any clear results so far, but I will report more a bit later.
I've spent a few more hours on the problem, repeating the bisection
several
a lot
of stack space, and thus fills up memory on x86_64. I've addressed
this in f25bcb8a4591 to get more explicit failure.
I've also started some bisection about where the problem comes from,
without any clear results so far, but I will report more a bit later.
Is Lukas Bulwahn still
On 10/22/2012 08:22 AM, Lukas Bulwahn wrote:
On 10/19/2012 04:35 PM, Makarius wrote:
On Fri, 19 Oct 2012, Lukas Bulwahn wrote:
Operations like Simplifier.context, Simplifier.inherit_context
should help here. Once that is repaired, I will see if the warning
can now be made an error
On 11/07/2012 10:41 PM, Gerwin Klein wrote:
On 08/11/2012, at 8:26 AM, Florian
Haftmannflorian.haftm...@informatik.tu-muenchen.de wrote:
Am 07.11.2012 22:22, schrieb Gerwin Klein:
If I run sessions manually, they work fine, but they fail in the cron job with
timeout (even small ones like
I think priority queues are roughly ordered lists (the priority is the
ordering). So, you could have a look at Pure/General/ord_list.ML
Lukas
On 10/24/2012 05:21 PM, Steffen Juilf Smolka wrote:
Hi,
is there an implementation of priority queues in the isabelle library?
Steffen
On 10/19/2012 04:35 PM, Makarius wrote:
On Fri, 19 Oct 2012, Lukas Bulwahn wrote:
Operations like Simplifier.context, Simplifier.inherit_context
should help here. Once that is repaired, I will see if the warning
can now be made an error that is more explicit about the reasons.
I am
On 10/19/2012 04:23 PM, Tjark Weber wrote:
Hi Lukas,
On Tue, 2012-10-16 at 18:23 +0200, Lukas Bulwahn wrote:
the testboard was repeatedly breaking down today---and I restarted it
multiple times to keep the illusion of a stable environment. I will
investigate tomorrow what is going wrong. Until
Hi Dmitriy,
If you update to changeset 89b118c0c070, the issue should be resolved.
Lukas
On 10/16/2012 01:41 PM, Dmitriy Traytel wrote:
Hi all,
the following produces a Loose bound variable with
Isabelle/4a15873c4ec9
theory Scratch
imports Main
begin
lemma finite {y |y. ∃x. y ∈ f x}
Hi Florian,
in the changeset e8400e31528a of the Isabelle repository, you moved the
theorem Pair_inject in the Product_Type theory into a section called
Legacy theorem bindings and duplicates.
In my current development, I rely on the theorem Pair_inject, and it is
the most suitable rule for
Hi all,
the testboard was repeatedly breaking down today---and I restarted it
multiple times to keep the illusion of a stable environment. I will
investigate tomorrow what is going wrong. Until then, I'll try my best
restarting it after a break-down as fast as possible.
Lukas
Hi Florian,
just for the record:
- I added those FIXMEs while adding the set_comprehension_pointfree
simproc.
- If this FIXME would have been a trivial exercise, I would have done it
immediately. However, moving is only possible after some further changes
in the simproc itself.
- In the
Hi Florian,
this sounds similar to ideas that (Alex and) Lars had to allow
find_theorems to search on all Isabelle sessions. As far as I know, they
have an implementation for this feature in their shelf.
Lukas
On 10/11/2012 02:44 PM, Florian Haftmann wrote:
Hi all,
recently I had the
Hi Florian,
Thanks for your feedback. The main developer Markus Kaiser is giving a
presentation next week and we will discuss further steps.
Here's a part of a private German discussion with Makarius that explains
how to switch back to the classical browser (in PG/Emacs).
in
On 10/09/2012 11:20 AM, Makarius wrote:
On Mon, 8 Oct 2012, Brian Huffman wrote:
I have a changeset that removes the set-definition features from the
{cpo,pcpo,domain}def commands in HOLCF, and it checks successfully on
testboard.
http://isabelle.in.tum.de/testboard/Isabelle/rev/a093798fa71b
It is probably due to my latest changeset in the
set_comprehension_pointfree simproc.
Lukas
On 10/10/2012 03:50 PM, Johannes Hölzl wrote:
Hi,
I tried to build AFP/Grith_Chormatic, but the simplifier fails in
Ugraphs.thy line 168:
using card_left_less_pair assms by simp
with the
On 09/24/2012 09:33 PM, Makarius wrote:
On Fri, 21 Sep 2012, Lukas Bulwahn wrote:
I am just at the moment trying to get it running again.
Lukas
On 09/21/2012 10:54 AM, Jasmin Christian Blanchette wrote:
Am 21.09.2012 um 09:18 schrieb Tobias Nipkow:
The testboard runs most of the AFP
Thanks to Dmitriy's effort, all AFP entries run successfully again.
Original Message
Subject:status (AFP)
Date: Fri, 21 Sep 2012 09:10:43 +0200 (CEST)
From: isat...@macbroy2.informatik.tu-muenchen.de (Isabelle )
To: undisclosed-recipients:;
The status of the
Hi all,
I have just installed the Isabelle development repository on one of the
remote machines.
With the new build system, the component management and PolyML 5.5, I
got a system up and running in less than 20 minutes.
In former times, it usually took me 20 minutes just to get an updated
On 07/28/2012 05:32 PM, Florian Haftmann wrote:
Hi Lukas,
I have corrected cs 6efff142bb54 by cs 7c497a239007, and have relaxed
the issue with Efficient_Nat a little (cs 084cd758a8ab, see below for a
short discussion). This has raised a couple of questions:
1. Why did the testboard not check
On 07/22/2012 10:29 AM, Florian Haftmann wrote:
text {*
FIXME -- Evaluation with @{text Quickcheck_Narrowing} does not work, as
@{text code_module} is very aggressive leading to bad Haskell code.
Therefore, we simply deactivate the narrowing-based quickcheck from here on.
*}
I do not
Hi all,
since 06/05/2012, I have not received any status (AFP) emails, although
it should have been failing the last days.
(After Isabelle:e7e647949c95, the theory LinearQuantifierElim was
failing, and I just fixed with AFP:96f043cb412e.)
Is the AFP test script still working properly?
Maybe
On 06/17/2012 06:36 PM, Florian Haftmann wrote:
Thanks. It asks me to set 'Environment variable ISABELLE_GHC '. So I uncomment the
line 'ISABELLE_GHC=/usr/local/ghc/$ISABELLE_PLATFORM/ghc'
Now it gives me another error message Compilation with GHC failed. Any
suggestion ?
PS, I work in a
On 05/30/2012 02:44 PM, Makarius wrote:
On Wed, 30 May 2012, Lukas Bulwahn wrote:
On 05/29/2012 02:01 PM, Makarius wrote:
* Admin/contributed_components within the repository documents
semi-formally which components may be included into a certain
version.
The mira experts should
On 05/25/2012 03:31 PM, Lukas Bulwahn wrote:
On 05/25/2012 02:17 PM, Makarius wrote:
On Fri, 25 May 2012, Lukas Bulwahn wrote:
On 05/23/2012 01:28 PM, Makarius wrote:
Dear All,
the current situation is as follows:
* As of Isabelle/c5f7be4a1734 the
http://isabelle.in.tum.de/repos/isabelle
On 05/23/2012 01:28 PM, Makarius wrote:
Dear All,
the current situation is as follows:
* As of Isabelle/c5f7be4a1734 the
http://isabelle.in.tum.de/repos/isabelle-release branch is merged
again with the main line.
* isatest is back testing http://isabelle.in.tum.de/repos/isabelle
Hi Christian,
For code generation purposes and especially Quickcheck, it is necessary
that the FinFun theory would be imported by any user.
With the new developments lifting and transfer, we are getting very
close that FinFun can be used without any further ado.
I do have some latest
On 04/20/2012 02:12 PM, Lukas Bulwahn wrote:
On 02/27/2012 02:31 PM, Makarius wrote:
On Mon, 27 Feb 2012, Lukas Bulwahn wrote:
A large part of Quickcheck's run time is spent in the code generator
calls, and the evaluation, which does mostly memory allocations and
deallocations.
I am
On 04/18/2012 08:26 PM, Florian Haftmann wrote:
Hi all,
- I would like to add a size limit to records beyond which no code generator setup
is performed. The main reason is that on sizes 200 fields or so, the setup
does not make any sense, but consumes very large amounts of memory (and
On 04/16/2012 09:13 AM, Christian Sternagel wrote:
Hi all,
On 04/03/2012 02:51 AM, Florian Haftmann wrote:
well, I suggest to augment the existing theory with lemmas transferred
from relpow to relpowp to emphasize that both worlds exists and that
lemmas can be found easier by find_theorems.
Hi Chris,
I have tested your changeset on the testboard, and a couple of AFP
theories break, cf.
http://isabelle.in.tum.de/testboard/Isabelle/report/edd1df5c8daf4109a6366801aaeff7fd
(Some errors are due to your changes, some are due to current work of
others.)
It might be good to provide some
The webpage on the Isabelle (community) wiki,
https://isabelle.in.tum.de/community/Administration_of_the_isatest_facilities,
summarizes the agreement of this thread.
If anyone wants to add or modify the page, feel free to do so.
Lukas
On 03/29/2012 09:29 AM, Gerwin Klein wrote:
On
I restarted all mira daemons now.
Lukas
On 03/29/2012 09:53 AM, Florian Haftmann wrote:
I guess someone must restart the mira deamons in order to run with the
adjusted configurations.
Florian
___
isabelle-dev mailing list
Hi Florian,
Thank you for your suggestions. We will take them into account.
On 03/28/2012 07:26 AM, Florian Haftmann wrote:
http://isabelle.in.tum.de/reports/Isabelle/rev/861f53bd95fe#l1.53
the name given to the derived theorem is unsatisfactory. Since it is
not a »code-only« theorem, it
I cannot build the IsarImplementation Manual on 9fc17f9ccd6c:
Maybe some latest change broke the document generation.
Lukas
Running HOL-Thy ...
HOL-Thy FAILED
(see also
/home/bulwahn/.isabelle/./heaps/polyml-5.3.0_x86-linux/log/HOL-Thy)
***
*** The error(s) above occurred in document
On 03/26/2012 02:10 PM, Makarius wrote:
On Sun, 25 Mar 2012, Brian Huffman wrote:
As of 2a1953f0d20d, Isabelle now has a new representation for binary
numerals
Execellent, this is a big step forward in this important reform. It
seems we now have the main parts in place, so that we can
On 03/23/2012 11:45 AM, Jesus Aransay wrote:
I know there is an alternative way to get that, by means of sparse
matrices (SparseMatrix.thy), but it demands translating every
operation over the matrix type to its equivalent version for sparse
matrices, which may be sometimes hard work.
Code
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum
On 03/21/2012 09:08 AM, Christian Sternagel wrote:
On 03/21/2012 05:05 PM, Lukas Bulwahn wrote:
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code
I hope changeset 2cdf5c71b818 in the AFP solves the issue.
Lukas
On 03/11/2012 01:02 PM, Brian Huffman wrote:
On Sun, Mar 11, 2012 at 12:09 PM, Tobias Nipkownip...@in.tum.de wrote:
One error in JinjaThreads was fixed, here is the next one:
*** Unknown fact list_all2_update_cong2 (line 467
Thanks a lot for your help.
A large part of Quickcheck's run time is spent in the code generator
calls, and the evaluation, which does mostly memory allocations and
deallocations.
I am surprised that this issue suddenly occurs now that it is its own
session. Maybe the many parallel
On 02/18/2012 10:18 AM, Florian Haftmann wrote:
How much relative time do the quickcheck examples in HOL-ex take?
According to my feeling time could be high to separate these into a
separate session, to facilitate maintenance.
I separated the Quickcheck-Examples from HOL-ex into an own session
On 02/24/2012 09:01 AM, Florian Haftmann wrote:
Accidentally I have pushed something into the main repository which
was still supposed to be tested. PLEASE IGNORE HEAD REVISION
0bd7c16a4200 and continue with the other head.
Sorry for this,
Florian
I was close to this mistake myself a
On 02/18/2012 10:18 AM, Florian Haftmann wrote:
How much relative time do the quickcheck examples in HOL-ex take?
According to my feeling time could be high to separate these into a
separate session, to facilitate maintenance.
Are there any voices pro or contra? IMHO the overhead when figuring
Just two comments:
First, the discussion about this should be on the isabelle mailing list,
not the isabelle developer's mailing list.
There has been a discussion just a few days ago that the developer's
mailing list is limited to arbitrary repository versions and the related
development
Hi all,
the latest failures of the isabelle test of the form:
/tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs::XX:
Conflicting definitions for `ad'
Bound at:
/tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs::XX-XX
On 01/11/2012 09:29 PM, Alexander Krauss wrote:
The real problem is in fact JinjaThreads. AFAIK, the only machine at
TUM where it can still build (in principle) is lxbroy10, but as Lukas
pointed out there are still some failures, cf.
On 11/30/2011 03:17 PM, Tobias Nipkow wrote:
Am 30/11/2011 12:27, schrieb Makarius:
This concerns Isabelle/3d6ee9c7d7ef:
Adding a global constant Quickcheck_Exhaustive.unknown with rather
generic notation ? to main HOL is a bit dangerous. The name unknown
is also a candidate for hide_const
On 12/08/2011 02:35 PM, Florian Haftmann wrote:
Dear all,
since my post on quotient and partiality created some confusion, I want
to cast some light on it from a more direct perspective.
Just a few short comments from my side:
Concerning »typedef«, we currently have two conflicting issues:
Quickcheck returns variable assignments as counterexamples, which
allows to reveal the underspecification of functions under test.
For example, refuting hd xs = x, it presents the variable
assignment xs = [] and x = a1 as a counterexample, assuming that
any property is false
On 11/30/2011 01:14 PM, Makarius wrote:
On Wed, 30 Nov 2011, Makarius wrote:
This concerns Isabelle/3d6ee9c7d7ef:
Adding a global constant Quickcheck_Exhaustive.unknown with rather
generic notation ? to main HOL is a bit dangerous. The name
unknown is also a candidate for hide_const
On 11/28/2011 10:41 PM, Makarius wrote:
On Mon, 28 Nov 2011, Lukas Bulwahn wrote:
many recent requests for adjusting the user-space behavior of typedef
would then rather apply to quotient_type.
Also, I do not see the clear advantage how the suggested change would
make the adjustments
On 11/29/2011 06:21 AM, Cezary Kaliszyk wrote:
When developing the quotient package we included the infrastructure
for defining quotient types with partial equivalence relations, however
since one of the main uses was supposed to be nominal (where its
always reflexive) we did not test the
On 11/17/2011 11:58 AM, Jasmin Christian Blanchette wrote:
Hi again,
When it comes to the AFP failure, there's a second AFP failure, in
JinjaThreads, that's obviously related to the servers' being down yesterday;
the Lam-ml-Normalization failure could be due to that, too. Lukas is helping
With changeset aa35c9454a95, HOL-Mutabelle compiles again.
Lukas
On 11/09/2011 06:16 PM, Makarius wrote:
In Isabelle/d17556b9a89b HOL-Mutabelle is broken:
HOL-Mutabelle FAILED
(see also
/Volumes/Macintosh_HD/Users/makarius/.isabelle//heaps/polyml-5.4.2_x86_64-darwin/log/HOL-Mutabelle)
***
On 10/27/2011 04:38 PM, Florian Haftmann wrote:
Nonetheless, we still have the real-based Library.random from ML for
the working programmer, because without it quickcheck performs really
bad.
AFAIR this has only been the case for the ancient SML quickcheck,
whereas my quickcheck implementation
Hi all,
JinjaThreads currently probably fails because of the changeset
6e422d180de8 (http://isabelle.in.tum.de/repos/isabelle/rev/6e422d180de8)
*** empty result sequence -- proof command failed
*** At command apply (line 2941 of
/home/kleing/afp/devel/thys/JinjaThreads/Compiler/JVMJ1.thy)
On 10/16/2011 10:06 PM, Alexander Krauss wrote:
On 10/16/2011 02:53 PM, Florian Haftmann wrote:
On lxbroy10, something is utterly wrong:
http://isabelle.in.tum.de/testboard/Isabelle/report/89d77033f6eb4dc196c199893871ae6d
Is anyone taking care for this?
Just tried to fix with
On 10/16/2011 10:06 PM, Alexander Krauss wrote:
On 10/16/2011 02:53 PM, Florian Haftmann wrote:
On lxbroy10, something is utterly wrong:
http://isabelle.in.tum.de/testboard/Isabelle/report/89d77033f6eb4dc196c199893871ae6d
Is anyone taking care for this?
Just tried to fix with
On 10/13/2011 10:52 AM, Florian Haftmann wrote:
Hi Lukas,
»removing checking of generated code because it fails on the mira
testing infrastructure due to a missing Pure image« – I don't quite
understand this. Why exactly is the check failing?
Florian
The issue can be observed at
On 10/03/2011 04:59 PM, Florian Haftmann wrote:
+text {* Definitions could be moved to Transitive_Closure if they are
of more general use. *}
is there any striking reason *not* to do so in the first place? At a
first glimpse I can't see anything which relates to Enum.thy in those
theorems.
Hello all,
the traditional isatest's AFP-Test did not report any failures the last
few days,
but the emerging testboard infrastructure mentions failures over the
last few versions, and the current tips
On 09/22/2011 11:36 AM, Peter Lammich wrote:
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
Legacy.thy that would not be imported by default, and would be
cleared out after each release. When upgrading Isabelle,
Thanks. I've set the JinjaThreads test to run every day now, at least until the
release.
In Munich, we now also use our number cruncher lxbroy10 to run the large
(non-frequently tested) AFP sessions within the new testing infrastructure.
This should give us some more light on failures of
Hello all,
Lars and I have taken over the maintenance of the reports and testboard
from Alex yesterday.
Today, due to some storage issues, we did not learn early enough about,
the testboard repository changed into an inconsistent state.
I reset the testboard repository to start with a clean
On 09/19/2011 01:56 PM, René Thiemann wrote:
Dear all,
There are still some improvements to the Haskell serializer and the code
generator I would like to get into the release.
After some discussions with Florian, the remaining changesets are about ready
and final, so I can probably commit
Hello all,
Are there any further things in the pipeline? In the final phase one
needs a bit more organization than the push first, fix later cycle
that occasionally happens outside this special season.
There are still some improvements to the Haskell serializer and the code
generator I
On 09/12/2011 07:29 PM, Florian Haftmann wrote:
Hi Lukas,
the rename
AssocList ~ AList_Impl
should sound
AssocList ~ AList
Nota bene:
T.thy – theory as intended to be used by other theoreis
T_Impl.thy – implementation for abstract type
Since ALists are not abstract, there is
On 09/09/2011 02:52 PM, Makarius wrote:
On Fri, 9 Sep 2011, Lukas Bulwahn wrote:
In my concrete case:
When running the compilation within the make command, I get:
*** exception Option raised
Exception- TOPLEVEL_ERROR raised
*** ML error
Whereas running it interactively in PG
Hello all,
lately, I have noticed that the exception handling within the
non-interactive execution has changed, disguising the true origin of
exceptions.
In my concrete case:
When running the compilation within the make command, I get:
*** exception Option raised
Exception- TOPLEVEL_ERROR
Changesets f523923d8182 and 3bc39cfe27fe should have resolved the issue.
Lukas
On 09/02/2011 11:40 AM, Lukas Bulwahn wrote:
The reason that this issue has just recently become apparent, is due
to changes 322d1657c40c ff. by Andreas Lochbihler. He assisted in
replacing (Stefan Berghofer's) SML
The reason that this issue has just recently become apparent, is due to
changes 322d1657c40c ff. by Andreas Lochbihler. He assisted in replacing
(Stefan Berghofer's) SML code generator invocations by generic code
generator invocations to enable the long-term removal of the SML code
generator.
Stefan Berghofer wrote:
Alexander Krauss wrote:
In particular, Stefan discovered that replacing inductive set
definitions by predicates was by no means as easy as everybody had
expected. One good example is the small-step relation from Jinja and
its various cousins. It had type ((expr * state)
On 08/19/2011 07:39 AM, Tobias Nipkow wrote:
Am 19/08/2011 00:00, schrieb Stefan Berghofer:
Alexander Krauss wrote:
I want to emphasize that the limitation of the code generator mentioned
here not only applies to sets-as-predicates but also to
maps-as-functions and other abstract types that
On 07/25/2011 10:25 AM, Makarius wrote:
On Sun, 24 Jul 2011, Alexander Krauss wrote:
Anyway, the standard procedure for removal of old stuff is to start
marking it as old or legacy in the NEWS, and emitting suitable
legacy_warnings.
I will follow that standard procedure, once all
On 07/24/2011 04:57 PM, Makarius wrote:
On Thu, 21 Jul 2011, Lukas Bulwahn wrote:
at the moment, we have two code generators in Isabelle:
1. An ancient code generator in Isabelle by Stefan Berghofer -
limited to SML without supporting type classes. Commands to invoke it
were code_module
On 07/22/2011 09:36 AM, Alexander Krauss wrote:
datatype foo =
deriving countable, finite,
Tobias also mentioned set_of, map_of, etc. But since these aren't
class instantiations (we have no constructor classes such as
functor), we end up with the good old generic datatype
On 07/22/2011 10:44 AM, Lukas Bulwahn wrote:
On 07/22/2011 09:36 AM, Alexander Krauss wrote:
datatype foo =
deriving countable, finite,
Tobias also mentioned set_of, map_of, etc. But since these aren't
class instantiations (we have no constructor classes such as
functor), we end up
Hello all,
at the moment, we have two code generators in Isabelle:
1. An ancient code generator in Isabelle by Stefan Berghofer - limited
to SML without supporting type classes.
Commands to invoke it were code_module and code_library.
2. A generic code generator in Isabelle by Florian
On 07/20/2011 09:34 PM, Florian Haftmann wrote:
Dear all,
with Cezary's guidance, I set up mira configurations for building the
proofs bundle from the HOL Light repository and for running the
HOL-Generate-HOLLight with that bundle, cf.
Hi,
Working with the development version, I have been noticing warnings ...
Bad binding:
Is there now a stricter guideline using or creating bindings that
Isabelle's developers should follow?
Lukas
___
isabelle-dev mailing list
On 07/08/2011 03:13 AM, Brian Huffman wrote:
I wrote to Florian about this exact issue back in February 2010.
Florian's recommended solution at the time was to add a new subclass
of archimedean_field that fixes the floor function and assumes a
correctness property about it. This solution is
Hello all,
this week, we, Johannes Hoelzl and me, gave a two-and-half-hour tutorial
to Isabelle at a workshop meeting of PhD students in computer science in
Dagstuhl (cf. http://www.model.in.tum.de/um/vernetzungstreffen/).
We used Isabelle/jEdit with some latest development snapshot and
On 05/30/2011 06:03 PM, Lukas Bulwahn wrote:
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
Hi Andreas,
the following ML line should do the job of adding the congruence rule in
your case:
setup {* Code_Preproc.map_pre (fn ss = ss addcongs [@{thm conj_cong}]) *}
Before we add yet another feature to the code generation setup in Isar,
we would like to understand your scenario.
Does
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
definition test where test xs = (last xs = 0)
Hi,
My changes caused this error.
I am working on different compilation schemes in Quickcheck.
Quickcheck registers its type-class based generator construction in the
Datatype package in the HOL image.
The complete Isabelle repository ran through (with all its datatypes),
but the Sigma
On 04/08/2011 01:03 PM, Stefan Berghofer wrote:
Quoting Lukas Bulwahn bulw...@in.tum.de:
Hi,
My changes caused this error.
I am working on different compilation schemes in Quickcheck.
Quickcheck registers its type-class based generator construction in
the Datatype package in the HOL image
On 01/19/2011 03:41 PM, Mathieu Giorgino wrote:
Hello all,
It seems there is a problem with the list_to_set_comprehension tactic for
terms containing a pattern matching on a datatype with a single constructor
with at least three arguments (It appears as a rather specific problem...).
On 01/11/2011 05:42 PM, Makarius wrote:
Changes for list_to_set_comprehension keep coming in, and it seems to
be not quite stabilized yet.
Where is the NEWS entry that tells users what to do in case of failure?
Here is the NEWS:
* New simproc that rewrites list comprehensions applied to
On 10/07/2010 09:11 AM, Florian Haftmann wrote:
I'm currently working on a package for generic type mappers. Leaving
aside matters like contravariance and such, a type mapper
map_k :: ('a_1 = 'b_1) = ... = ('a_n = 'b_n)
= ('a_1, ..., 'a_n) k is = ('b_1, ..., 'b_n) k
for an n-ary
93 matches
Mail list logo
