On Thu, Mar 29, 2012 at 7:50 AM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
As it is now, theory »Code_Nat« is
not announced that prominently, but this is not that critical.
We should at least put an announcement in NEWS about Code_Nat.
However, you have talked about
However, you have talked about making the binary representation for
nat the default in HOL-Main, i.e. merging Code_Nat into the Nat/Num
theories. Are you still interested in doing this?
Definitely, among other related things. But I'm not very optimistic
this can be done before the end of
I have
* linked the existing OpenJDK 1.6 on macbroyXYZ to
/home/isabelle/contrib_devel/jdk
* and added one line to the mira default settings to set
ISABELLE_JDK_HOME accordingly
in order to provide and ad-hoc setup for the mira tests.
I have no idea how platform-indepedent this symlink is, so
On 29/03/2012, at 4:31 PM, Tobias Nipkow wrote:
Am 28/03/2012 23:30, schrieb Gerwin Klein:
On 29/03/2012, at 6:11 AM, Makarius wrote:
On Wed, 28 Mar 2012, Florian Haftmann wrote:
Once there has been the idea that everyone having commit access to the
Isabelle master repository (POSIX
I guess someone must restart the mira deamons in order to run with the
adjusted configurations.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
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
On Wed, 28 Mar 2012, Cezary Kaliszyk wrote:
- The code is shorter and cleaner.
For those that would like to inspect the code it is at:
http://cl-informatik.uibk.ac.at/~cek/import.tgz
Wow, I am impressed by the brevity of it. You should mention the secret
On Thu, Mar 29, 2012 at 8:04 PM, Makarius makar...@sketis.net wrote:
Wow, I am impressed by the brevity of it. You should mention the secret
http://cl-informatik.uibk.ac.at/~cek/proofs which is a bzip stream to be
uncompressed, before it can be used with import_file in the example.
That's the
