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 norm
| "f (Foo (Suc n)) = f (Foo n)"
> | "f (Bar x) = f x"
> by pat_completeness simp_all
> termination by(relation "measure (foo_size size)") simp_all
>
> Andreas
>
>
> 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 all the infrastructure built around it (e.g.
> size functio
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
Totally agree. Considering the tools they had available, they are
geniuses in my book. But there *is* a parallel with the workers who
build the pyramids. Although free, their skeletal remains clearly
show a life of hard labour and misery. Wished Isabelle developers
somehow had moved on from that
On Thursday, April 4, 2013 at 12:42:42 (+0200), Makarius wrote:
> On Thu, 4 Apr 2013, Thomas Sewell wrote:
>
> > David's investigation explains a problem we had a few years ago where
> > some custom tactics of mine were killing my colleagues' ProofGeneral
> > sessions when they encountere
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.
> >
> > Tri
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"
> &g
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
new_ty
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 scenari
Hi Christian,
Did this already get into the Distribution and AFP?
Christian
On Thursday, August 30, 2012 at 16:19:08 (+0900), Christian Sternagel wrote:
> Sorry! I forgot to commit my last change (and sorry for the many typos
> in my last email). - chris
>
> On 08/30/2012 03:36 PM, Christ
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 norm
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
Dear Makarius,
On Thursday, August 23, 2012 at 15:23:49 (+0100), Makarius wrote:
> On Wed, 22 Aug 2012, Christian Urban wrote:
>
> > I am used to building the nightly snapshots, which in the olden days was
> > conveniently done by the build script. Well, times chang
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 HOL-Nominal
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 hav
(+0100), Makarius wrote:
> On Mon, 6 Aug 2012, Christian Urban wrote:
>
> > 1) I transferred two "old" IsaMakefile/ROOT.ML files to a
> > "new" ROOT like:
> >
> > session Nominal2! in "Nominal" = HOL +
> >
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 tw
On Thursday, May 24, 2012 at 12:14:14 (+1000), Thomas Sewell wrote:
> It looks like you want to implement a simproc.
Thanks a lot for the suggestion. My first "iteration"
was implemented via a solver. It worked. But then,
inspired by the neq-simproc in HOL.thy, I already
modified my code to be
es. This is the approach that fits with the general design of
> the simplifier. Not the structure you want? Too many inequalities? In
> that case you really need a guided solver - giving the simplifier
> opportunities for wild exploration will just slow everything down.
>
> Yours,
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 ⟹
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 meant
On Thursday, May 10, 2012 at 18:46:04 (+0100), Lukas Bulwahn wrote:
>
> In the short term, we could move the FinFun theory into the HOL library
> of the development version after Isabelle 2012 and the AFP 2012 has been
> released, if we agree that this moves this contribution in the right
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 (%
Hi All,
Somebody recently added in the NEWS the entry
Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset,
UNION_eq_Union_image, Union_def
Quoting Florian Haftmann :
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 set-type. They had an instance
for sets and permuta
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;
>
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
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 a
Hi Walther,
Here my guess what is going on:
Given
val t = @{term "a + b * x = (0 ::real)"};
val pat = parse_patt thy "?l = (?r ::real)";
val precond = @{term "l is_polynomial"};
we match
val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
in order to get an environmen
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 antiquota
Thomas Sewell writes:
>
> BTW, should I have known this already? Is there some part of the
> documentation that I should have read, but have overlooked?
Sort of. Both functions are used in an example in the Programming
Tutorial[*] on page 19. What the function check_term does is a bit
more
> I am working with the Isabell/HOL system which is hosted by default
> on the PolyML system. I have found a strange syntax construct in
> some of the source code files consisting of @{ ...some
> verbage ... } , examples below. I have searched the ML library
> pages and the PolyML doc
This is NOT an April Fools' Joke ;o)
Hi,
almost a year ago we started a project to lower the entry
barrier for users to program on the ML-level of Isabelle.
We now have a draft for the Isabelle Programming Tutorial.
See
http://isabelle.in.tum.de/nominal/activities/idp/
As usual with such docu
sible
topics of interest at
http://isabelle.in.tum.de/nominal/activities/idp/
but we are more than welcome to the Isabelle community's input.
Best wishes,
Christian Urban
Larry Paulson
Michael Norrish
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 effor
39 matches
Mail list logo
