[isabelle-dev] New testing infrastructure

Dear Isabelle developers, as promised last week, I've been working on a new testing infrastructure for Isabelle. Here's what works now: * There is a live Jenkins instance at [1]. It is publicly available and runs on a virtual machine provided by the department's

[isabelle-dev] Future of permanent_interpretation

Recently in private discussion there was the question what the supposed future of permanent_interpretation is supposed to be. It looks as follows: Step 1) * Put »permanent_interpretation« into Pure directly. Step 2) * Careful revisiting of the documentation to emphasize the

Re: [isabelle-dev] Definite name for case combinator on products [was: NEWS]

In fb95d06fb21f, find my attempt to reach a stable status again after opening too many loose ends. * The combinator is named »case_prod« uniformly; no aliasses remain, in order not to obfuscate the now reached state of uniformity. * The most popular theorem names with »split« are retained (see end

[isabelle-dev] Mac OS X 10.11 (El Capitan)

Apple has released OS X 10.11 (El Capitan) recently. I have updated my test machine some days ago and made a few sanity checks. So far the situation looks good concerning Isabelle. A test version is available here: http://www4.in.tum.de/~wenzelm/test/Isabelle_07-Oct-2015 Are there further

Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)

I have also upgraded and I find that everything still works the same as before. The only restriction on an unsigned application is that the first time you open it, you need to select the “open” menu item rather than simply double-clicking on some file. Then you need to confirm that you want the

[isabelle-dev] Explicit option "open" for code_reflect

Hi Florian, Between Isabelle 2014 and 2015, the option "open" appeared for the command export_code, and by default the reflection minimizes the exported code. Would it be acceptable for code_reflect to also have a similar option "open"? As a draft example, here is a list of modifications

Re: [isabelle-dev] Mac OS X 10.11 (El Capitan)

On Tue, 13 Oct 2015, Larry Paulson wrote: The only restriction on an unsigned application is that the first time you open it, you need to select the “open” menu item rather than simply double-clicking on some file. Then you need to confirm that you want the application to open. In theory it