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 interface is supposed to do.
Actually I did never use these
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 interface
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
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.
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
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
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 of
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 purpose.
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
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 @
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 memory
11 matches
Mail list logo
