Re: [isabelle-dev] status (AFP)

2012-10-04 Thread Makarius
On Thu, 4 Oct 2012, Gerwin Klein wrote: This is now done, AFP_big has been retired, and afp_build updated accordingly. Great. I have removed one more letter in AFP/c9d12d55c3a6. BTW, my afp_build was more like an example. Feel free to reshape the standard build process in the way you see

Re: [isabelle-dev] status (AFP)

2012-10-04 Thread Florian Haftmann
Florian also has an older attempt at some testafp tool in the AFP repository, which should be obsolete now. This is obsolete now. Anyone still having stocks there? Florian -- PGP available:

[isabelle-dev] typedef (open) legacy

2012-10-04 Thread Christian Urban
Hi, Closed type definitions with typedef new_type = some set are considered legacy. The warning message suggests to use typedef (open) new_type = some set but as far as I can see, this does not introduce a definition for the set underlying the type. For example the theorem

Re: [isabelle-dev] Locale interpretation with mixins

2012-10-04 Thread Florian Haftmann
Hi again! On our running gag list with have at least these related issues: * codgeneration as sketched above * behaviour of the Simplifier on seemingly atomic constants c (due to abbreviations) that are actually of the form loc.c x y z * stability and expectedness of

[isabelle-dev] An note on code generator bookkeeping and the code generator preprocessor [was: Locale interpretation with mixins]

2012-10-04 Thread Florian Haftmann
The current infrastructure has only a preprocessor applied *after* the internal bookkeeping (for reasons I will explain in a separate, long promised mail), so this would add further complexity here. What sets the code generator apart from other tools is that theorems are never stand-alone but

[isabelle-dev] Missing Isabelle component

2012-10-04 Thread Lawrence Paulson
Does anybody understand the attached message, which seems to involve the new build system? Larry ~/isabelle/Repos/src/HOL: isabelle build HOL-ex ### Missing Isabelle component: /Users/lp15/.isabelle/contrib/exec_process-1.0.2 Running HOL-ex … ~/isabelle/Repos/src/HOL: hg id 74ad6ecf2af2 tip

Re: [isabelle-dev] Missing Isabelle component

2012-10-04 Thread Tobias Nipkow
I believe you need to do isabelle components -a and it will download all missing components. It's a really neat system. Tobias Am 04/10/2012 15:47, schrieb Lawrence Paulson: Does anybody understand the attached message, which seems to involve the new build system? Larry

Re: [isabelle-dev] typedef (open) legacy

2012-10-04 Thread Brian Huffman
On Thu, Oct 4, 2012 at 2:17 PM, Makarius makar...@sketis.net wrote: On Thu, 4 Oct 2012, Christian Urban wrote: Closed type definitions with typedef new_type = some set are considered legacy. The warning message suggests to use typedef (open) new_type = some set but as far as I can

Re: [isabelle-dev] typedef (open) legacy

2012-10-04 Thread Christian Urban
Thanks a lot for all replies! Christian On Thursday, October 4, 2012 at 14:17:48 (+0200), Makarius wrote: On Thu, 4 Oct 2012, Christian Urban wrote: Closed type definitions with typedef new_type = some set are considered legacy. The warning message suggests to use

Re: [isabelle-dev] Isabelle/jEdit output panel

2012-10-04 Thread Christian Sternagel
Thanks! That's a great change. - Now that the output panel is based on the same technology as the main buffer, would it be feasible to include also the output panel when a search on all buffers is done. - An old story (but maybe now it's easier to realize?): It would also be great if