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
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:
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
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
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
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
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
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
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
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
10 matches
Mail list logo