Hi Clemens,
>> the story behind is not about syntax. It is really about the
>> simultaneous definitions. For a motivation, you can have a look at the
>> tutorial on code generation, section »Further issues«, »Locales and
>> interpretation«, where the pattern behind interpretation plus definition
On 04/18/2012 08:26 PM, Florian Haftmann wrote:
Hi all,
- I would like to add a size limit to records beyond which no code generator setup
is performed. The main reason is that on sizes> 200 fields or so, the setup
does not make any sense, but consumes very large amounts of memory (and time)
On 19/04/2012, at 4:26 AM, Florian Haftmann wrote:
> Hi all,
>
>> - I would like to add a size limit to records beyond which no code generator
>> setup is performed. The main reason is that on sizes > 200 fields or so, the
>> setup does not make any sense, but consumes very large amounts of me
On Wed, 18 Apr 2012, Christian Sternagel wrote:
it's very nice that after sledgehammer found a proof command to finish a
proof, I can simply click on this command in the output buffer to
include it in the main buffer! A slight oddity is that this merges
lines. E.g.,
lemma "⟦xs @ ys = ys @
Hi Florian,
Thanks for the clarification.
Its purpose
might have been to make the interpretation notationally simpler.
the story behind is not about syntax. It is really about the
simultaneous definitions. For a motivation, you can have a look at the
tutorial on code generation, section »Fu
> Does anybody have experience with the more recent "hg rebase"? An early
> version of it 3 years ago was causing problems, but one can probably
> expect this to be ironed out now.
I nowadays use »hg rebase« regularly, most times with the idiom »hg pull
--rebase«, and it seems to serve its purpos
I have skimmed over the NEWS and found a lot of things to consolidate,
rearrange or even correct. I would like to encourage all contributors
to do the same; there are a lot of rather promiment things (e.g.
Transitive_Closure.ntrancl) which could be moved before all those rather
technical theorem
Hi all,
>> Moreover NEWS in that version has oddities like this:
>>
>> rel_comp_def ~> rel_comp_unfold
>>
>> and later
>>
>> rel_comp_unfold ~> relcomp_unfold
>>
>>
>> In the time immediately before the relase (which is now) the NEWS should
>> reflect the perspective for end-users of the official
Hi all,
> - I would like to add a size limit to records beyond which no code generator
> setup is performed. The main reason is that on sizes > 200 fields or so, the
> setup does not make any sense, but consumes very large amounts of memory (and
> time). Switching it off gets rid of almost all
Hi all,
> The overloading rules are quite tricky. I don't understand why the first
> instantiation requires a definition of sup_hf (including the type in the
> constant name), while the second one simply requires a definition of minus.
> Perhaps because there is an explicit type in the first in
Hi Clemens,
> If you follow up the imported theory, you will find some code that
> provides a clone of the interpretation command (under the same name!)
> with some added functionality (definitions).
> Its purpose
> might have been to make the interpretation notationally simpler.
the story behin
Hi Alex,
> while backporting HOL/Library/Set_Algebras to use type classes again (a
> remaining point of the 'a set transition),
thanks for doing this!
> I noticed that there is now a
> clone of that file in HOL/ex.
> What should we do with the clone? Are there maybe other examples that
> can de
On Mo, 2012-04-02 at 13:45 +0200, Makarius wrote:
> On Mon, 26 Mar 2012, Peter Lammich wrote:
>
> > I tried to follow the approach done in the cancellation simprocs,
> > getting something like:
> >
> > fun assn_simproc_fun ss credex = let
> >val ctxt = Simplifier.the_context ss
> >val ([r
On Wed, 18 Apr 2012, Johannes Hölzl wrote:
When the testboard gives me green light I will tomorrow also push a
reworked Probability theory which only takes 2 min to build instead of 5
min as before. I also want to push a new version of the Floats which
uses the new lifting infrastructure.
B
When the testboard gives me green light I will tomorrow also push a
reworked Probability theory which only takes 2 min to build instead of 5
min as before. I also want to push a new version of the Floats which
uses the new lifting infrastructure.
Both changes do not change any ML files, and there
In preparation of the release, the following test website is now
available: http://www4.in.tum.de/~wenzelm/test/website/
So far this is just for warming up, and to see pending issues of overall
system integration. I have already updated many of the contributing
components: Scala, Java, Emacs,
On Wed, 18 Apr 2012, Gerwin Klein wrote:
If 3) means "configuration option" in the sense of Config.T, here is
the canonical 1-liner to make one for a package:
val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K
9);
Yes, that's what I meant. It's easy to set up, but
Am 18/04/2012 04:23, schrieb Christian Sternagel:
> +1 for <--> (since it would agree, as Tobias pointed out, with the established
> =>, ==>, ->, -->).
Thanks for actually referring to the topic at hand. The discussion has gotten
completely off topic and became quite fundamentalist. I was merely s
On 04/18/2012 03:56 PM, Christian Sternagel wrote:
On 04/18/2012 03:42 PM, Lawrence Paulson wrote:
How do you do “show me", “commands", “find theorem", “settings", etc?
I believe you're supposed to remember commands for all of those items
and type them explicitly. That's not what a user interfac
19 matches
Mail list logo
