Sorry about being a harbinger of bad news. But
this message about dead worker threads shows up
pretty frequently with me. Though it has not caused
any problems I am aware of. My guess is that I notice this
message already for at least a year. It is in fact
so frequent that I assumed this is
On 04/08/13 21:20, Christian Urban wrote:
On Sunday, August 4, 2013 at 20:32:50 (+0200), Dmitriy Traytel wrote:
I.e. everything that is defined by the new package and
falls into the fragment of the old package can be registered as an old
datatype benefiting from
On Sunday, August 4, 2013 at 20:32:50 (+0200), Dmitriy Traytel wrote:
I.e. everything that is defined by the new package and
falls into the fragment of the old package can be registered as an old
datatype benefiting from all the infrastructure built around it (e.g.
size function,
On Wednesday, July 17, 2013 at 13:43:34 (+0900), Christian Sternagel wrote:
@all: please let me know, in case anybody finds localized ad-hoc
overloading useful.
An aside: I'm currently using localized ad-hoc overloading for a port of
Nominal2's permutation type, where I use
On Sunday, February 17, 2013 at 17:06:46 (+0100), Tjark Weber wrote:
On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote:
* Sledgehammer spontaneously acts asynchronously of certain open
problems in the text, depending on certain parameters like time outs.
Triggering
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
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
On Wednesday, September 5, 2012 at 13:24:27 (+0200), Makarius wrote:
On Tue, 4 Sep 2012, Lars Noschinski wrote:
As an user, an easy method to test whether the current set of
assumptions still fit one of the pending goals is fix P show P sorry.
As I don't know any scenario where
On Wednesday, August 29, 2012 at 21:45:35 (+0200), Makarius wrote:
It is still used for isatest runs, but it does not have to be made public
as a crippled distribution that lacks most add-on components.
If it is only a small effort, I am happy to keep
it. The add-on components can
On Thursday, August 23, 2012 at 22:37:22 (+0200), Makarius wrote:
On Thu, 23 Aug 2012, Christian Urban wrote:
(1) copying etc/settings, etc/components and contrib/* from the
current working snapshot
Wait, this sounds suspicious. What is the current working snapshot
Dear All,
I am used to building the nightly snapshots, which
in the olden days was conveniently done by the build
script. Well, times change. ;o)
I remember (and again verified just now) that with the
snapshot from 14 August I can build Isabelle with
./bin/isabelle build -v -s -c
On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote:
Tjark, you have no business here.
I assume something got here lost in translation.
Otherwise, we should all make reasonable effort
to welcome everybody on both, the isabelle-users
and isabelle-dev lists. After all, we like to
On Monday, August 6, 2012 at 12:09:54 (+0200), Makarius wrote:
Did everybody try the isabelle build tool? Are there any problems left,
apart from retraining fingers after 16 years of usedir/make/makeall?
I just did. Building of heaps worked nicely. But two questions:
1) I transferred two
the simplifier
opportunities for wild exploration will just slow everything down.
Yours,
Thomas.
On 23/05/12 02:23, Christian Urban wrote:
Dear All,
Assuming that this is about the bowels of the simplifier,
I hope this is the right place to ask the following question
Dear All,
Assuming that this is about the bowels of the simplifier,
I hope this is the right place to ask the following question.
The simplifier has a subgoaler, which helps with rewriting
conditional lemmas. This simplifiying/subgoaling process seems
to be not transitive (probably is not
On Tuesday, May 22, 2012 at 20:59:28 (+0200), Tobias Nipkow wrote:
but am at least as confused as you are:
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
atom v ♯ (x1, x2) ⟹ atom v ♯ x1
[1]Applying instance of rewrite rule ??.unknown:
?a1 ♯ ?x1.1 ⟹ ?a1 ♯ ?x2.1 ⟹ ?a1 ♯
Dear All,
In Nominal I am usually relying on types that are defined
in HOL or that I define myself. However, I now came across
the FinFun development in the AFP by Andreas Lochbihler (thanks
to Larry). The finfun type seems to be rather useful to Nominal
users, since it has finite support, in
I was about to suggest the same as Andreas. For what it is
worth, here is my proof of this lemma.
lemma sorted_merge_induct[consumes 1, case_names Nil IH]:
fixes key::'b = 'a
assumes sorted (map key xs)
and !!xs. P xs []
and !!xs y ys. sorted (map key xs) == P (dropWhile (%x. key x
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:
I will now examine HOL-Nominal more closer, and after that come up with
a next report about the distribution.
There should be no problems in principle.
Early versions of Nominal (1) worked perfectly
with an explicit
Hi,
I just applied in a proof-script the following tactic
apply(auto simp add: f_def dest: l3)
and received the error message
*** exception Bind raised (line 934 of raw_simplifier.ML)
*** At command apply
Is this supposed to happen? f_def is from a function
I defined and l3 is a
Makarius writes:
The check_conv function also provides some extra trace, if
simp_trace/simp_debug is enabled. See the sources:
trace_thm (fn () = Proved wrong thm (Check subgoaler?)) ss thm';
trace_term false (fn () = Should have proved:) ss prop0;
NONE
I am not sure whether this is relevant, but
I have recently introduced a similar feature in
Nominal2. There the problem is that one often
defines several mutual-recursive nominal
datatypes, like
nominal_datatype
foo1 = ..
and foo2 = ..
and foon = ..
with n being
Hi Nils,
Nils Jähnig writes:
Hi,
1)
i'm reading the cook book, and in chapter 6, page 135 on the bottom
(latest draft from August 28th) , there is a piece of code including
Simplifier.simproc_global_i, which gives an error.
i went with simproc_i, this seems ok.
This is
On the topic of Mercurial: There is a nice 6-part
tutorial about it at
http://hginit.com/01.html
Maybe too basic for the seasoned users, but funny
nonetheless. And an example for a very crisp-clear
piece of writing.
Christian
Makarius writes:
On Wed, 3 Mar 2010, Brian Huffman wrote:
Dear Walther,
About your second question: there is a section
about using the function Pattern.match in the
Programming Tutorial ([1], Section 3.3). It should
explain how to do such pattern match examples.
The main contortion below probably comes from the
parsing of input. Since the
Lawrence Paulson writes:
Florian has suggested making sledgehammer available earlier in the
construction of Main, before PreList at least. This could be useful
to developers. However, it requires Hilbert_Choice, which must also
be introduced earlier. We previously put some effort
26 matches
Mail list logo
