Re: [isabelle-dev] Changes to the locale syntax

2015-10-30 Thread Makarius
On Wed, 28 Oct 2015, Clemens Ballarin wrote: I'm planning two moderate changes to the locale syntax: * The default of qualifiers in locale expressions will change from optional ("?") to mandatory ("!") in the context of "locale" and "sublocale". This brings these commands in line with

[isabelle-dev] Repository version of Isabelle on Windows 7

2015-10-30 Thread Anders Schlichtkrull
I am trying to install the repository version (f2e51e704a96) of Isabelle on Windows 7 using Cygwin by following README_REPOSITORY. Cygwin with Perl and Mercurial are installed, so I follow step 2 of README_REPOSITORY: Anders@r099121 /cygdrive/c/repo-isabelle $ uname -a CYGWIN_NT-6.1-WOW

Re: [isabelle-dev] Repository version of Isabelle on Windows 7

2015-10-30 Thread Makarius
On Fri, 30 Oct 2015, Anders Schlichtkrull wrote: Unpacking "/cygdrive/c/Users/Anders/.isabelle/contrib/csdp-6.x.tar.gz" tar: This does not look like a tar archive gzip: stdin: unexpected end of file tar: Child returned status 1 tar: Error is not recoverable: exiting now You see that I get an

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

2015-10-30 Thread Makarius
On Thu, 29 Oct 2015, Florian Haftmann wrote: I have not spend any thoughts whether there could be terminaton issues. Is there any argument beyond the absence of counterexamples that that can never happen? Standard batch build prints relatively few terms, so this is not yet significant as a