Hi Andreas,
> See now 788730ab7da4, which replaces all code_abort in HOL/Library with
> Code.abort.
> There are still two code_aborts in HOL (in Predicate and Enum) that
> Code.abort should subsume, but Code.abort can only be defined in
> String.thy due to the error message parameter it takes, and
On Thu, 26 Sep 2013, Peter Lammich wrote:
And the unpacked folder does not contain all necessary files
The bundled heap images were already discontinued in Isabelle2013 -- this
became possible due to isabelle build and getting rid of non-portable Unix
"make". Consequently, users have a few
On Thu, 26 Sep 2013, Lars Noschinski wrote:
On 26.09.2013 10:01, Peter Lammich wrote:
I cannot unpack the tar-file. My Linux (Ubuntu 12.04.2 LTS) gives me a
bunch of error messages:
tar: Ignoring unknown extended header keyword `SCHILY.ino'
tar: Ignoring unknown extended header keyword `SCHILY
On 26.09.2013 10:01, Peter Lammich wrote:
I cannot unpack the tar-file. My Linux (Ubuntu 12.04.2 LTS) gives me a
bunch of error messages:
tar: Ignoring unknown extended header keyword `SCHILY.ino'
tar: Ignoring unknown extended header keyword `SCHILY.nlink'
tar: Ignoring unknown extended header
Correction: The file unpacks correctly, the messages seem to be only
warnings.
I forgot to build the logic, immediately starting "isabelle emacs".
Peter
On Do, 2013-09-26 at 10:01 +0200, Peter Lammich wrote:
> I cannot unpack the tar-file. My Linux (Ubuntu 12.04.2 LTS) gives me a
> bunch of err
I cannot unpack the tar-file. My Linux (Ubuntu 12.04.2 LTS) gives me a
bunch of error messages:
tar: Ignoring unknown extended header keyword `SCHILY.ino'
tar: Ignoring unknown extended header keyword `SCHILY.nlink'
tar: Ignoring unknown extended header keyword `SCHILY.dev'
...
And the unpacked f
