Thanks for your input, I have added some of your lemmas to List (and will write
to you about separately).
No, there is no fixed process for adding such contributions. Until it becomes a
nuisance ;-) you are welcome to post them here or send them to some active
developer.
Tobias
Am 16/03/2012 10:
On Mon, Mar 26, 2012 at 7:23 PM, Makarius wrote:
> On Mon, 26 Mar 2012, Lukas Bulwahn wrote:
>
>> This problem is reproducible on our testboard servers. At the moment, all
>> tests of changesets after 2a1953f0d20d have to be manually aborted because
>> of that reason. I hope you find a solution qu
On Mon, 26 Mar 2012, Lukas Bulwahn wrote:
This problem is reproducible on our testboard servers. At the moment,
all tests of changesets after 2a1953f0d20d have to be manually aborted
because of that reason. I hope you find a solution quickly, otherwise we
should deactivate the Proofs-Lambda th
Hi all,
Referring to Isabelle-2011-1
(If this post belongs to the users list, feel free to answer it there)
I want to write a simplification procedure, that gets in a term t,
does some transformations on it to obtain a term t', then invokes the
simplifier (with some customized simpset) to prove
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 start
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 start consolidating
towards the release over
On Mon, 26 Mar 2012, Makarius wrote:
In practice, it means that people hooked in the repository version of
Isabelle/Scala and jEdit need to have JAVA_HOME or ISABELLE_JDK_HOME set
explicitly! I think Mac OS X does that by default, but probably not Linux
nor Windows.
In fact, the Mac OS X de
On Thu, 22 Mar 2012, Sascha Boehme wrote:
When the JDK is not given in the PATH variable, the command "isabelle jedit"
may fail with
./build-jars: line 189: jar: command not found
This is at least the case for hg id 08c22e8ffe70.
The problem occurs with Cygwin where the JDK is provided as a
Hi Brian,
Good work!
> There are still a couple of loose ends to take care of, which are
> currently marked with "BROKEN" in the sources:
>
> * Nitpick_Examples/Integer_Nits.thy: A call to nitpick on a goal with
> negative numerals doesn't work. I expect the problem originates in
> Tools/Nitpick
