[isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

isabelle: f1b257607981 tip afp: 1a688183b05a tip Any idea what is going on here? Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de Running ConcurrentGC ... Running MonoBoolTranAlgebra ... Running

Re: [isabelle-dev] Future of permanent_interpretation

For further discussion, see now fd4ac1530d63, particulary src/Pure/Isar/interpretation.ML and 5.7.3 »Locale interpretation« in *isar-ref*. This goes along the following lines: * »Interpretation« in general is used as generic heading for every kind of intepretation into different destination

Re: [isabelle-dev] code abbreviation for mapping over a fixed range

See now 9a51e4dfc5d9. Florian Am 12.11.2015 um 10:58 schrieb Jose Divasón: > Hi Bertram, Christian and Bertram, > > I would like to put my two cents in this topic. I have done a simple > experiment about this using my AFP entry about the QR decomposition, > where a strong use of

Re: [isabelle-dev] the function "real"

>> There are a great many examples of theorems involving various coercion >> functions and the relations =, <, <=. In a number of cases, the “real” >> versions were declared as [iff]-rules, while the “of_nat/of_int” >> versions were declared as [simp]-rules only. When identifying the two, >> I

[isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

Hi, Can someone please apply the attached patch to Isabelle for me? It does three things: - generalises Imperative_Quicksort to work on linearly-ordered, heap-representable types, and not just nat - renames Sublist to List_Sublist to avoid clashing with HOL/Library/Sublist - mildly weakens the

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

… and this time with the patch … > On 15 Nov 2015, at 22:15, Peter Gammie wrote: > > Hi, > > Can someone please apply the attached patch to Isabelle for me? > > It does three things: > - generalises Imperative_Quicksort to work on linearly-ordered, > heap-representable

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

MonoBoolTranAlgebra was failing due to my change in Isabelle/90f54d9e63f2 and the removal of theorem fun_eq in favour of arg_cong (I have not investigated when this happened, but just adapted the proof scripts), see changesets 53f94abb8704 and 0377b757f016. Presburger-Automata had a looping

Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts

On Sat, 3 Oct 2015, Rafal Kolanski wrote: My priority at the moment is to see a release of jEdit, before we enter the critical release phase for Isabelle2016 -- presumably at the start of the Winter season here in the north. Once it is there, I will update the jedit_build component

[isabelle-dev] CGSCreateKeyboardEvent

Larry, I am forwarding this to isabelle-dev since more people might have seen it. From a distance it looks to me like a problem of jdk-8u66, but Google does not know anything about it yet. The Isabelle2016 release is timed to happen shortly after the next jdk-8 release. This gives that

Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML

On 15/11/15 02:24, Makarius wrote: > On Fri, 13 Nov 2015, Rafal Kolanski wrote: > >> On 12/11/15 16:45, Japheth Lim wrote: >>> [...] >>> A lot of space could be saved if Isabelle saves heaps in this way. For >>> our L4.verified project we found a 7× reduction in size. >> >> I would like to add

Re: [isabelle-dev] Isabelle/jEdit - Sidekick

On Tue, 10 Nov 2015, Mathias Fleury wrote: in the sidekick there is a "sub-panel"^1 below the sidekick (see the red rectangle in the joint screenshot). Is there a way to have line breaks in it? The difference between it and the tooltips that appear in the sidekick, is that the tooltips

Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts

On 16/11/15 07:14, Makarius wrote: > I have lost track of the status of this thread, with its various > side-threads on isabelle-users, isabelle-dev, and private mail. All the patches I have sent out are still in effect w.r.t font rendering. > In the meantime the situation is as follows: > > *