I've got it. No problems with Isabelle.
Larry
On 2 Sep 2011, at 16:20, Jasmin Blanchette wrote:
> Am 02.09.2011 um 17:12 schrieb Makarius:
>
>> Did anybody get Mac OS Lion already?
>
> Not that I'm aware of.
>
> Jasmin
>
> ___
> isabelle-dev mailing
Am 02.09.2011 um 17:12 schrieb Makarius:
> Did anybody get Mac OS Lion already?
Not that I'm aware of.
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Fri, 2 Sep 2011, Jasmin Christian Blanchette wrote:
Are there any changes in the bundled "components" that need to be taken
care of? This always requires a few weeks to test on all available
platforms.
There's a new bundle for E 1.4, in "~isabelle/contrib_devel/e-1.4.tgz".
I didn't bothe
On Fri, 2 Sep 2011, Jasmin Blanchette wrote:
We should develop some feeling in which direction to move for the
source generation business. Anyway, is this mission critical for the
upcoming release?
No, not at all. It's not mission critical for any release. I've noticed
the problem when runn
Hi Makarius,
> Are there any changes in the bundled "components" that need to be taken care
> of? This always requires a few weeks to test on all available platforms.
There's a new bundle for E 1.4, in "~isabelle/contrib_devel/e-1.4.tgz". I
didn't bother with PowerPC this time; affected users
Hi Makarius,
> I have also thought again about 'unfolding' as such: it might actually
> qualify as preserving textual structure and thus as something that can be
> included in the textual scope for `...` -- assuming it will someday really
> cease to perform arbitrary simplification by accident.
On Thu, 25 Aug 2011, Florian Haftmann wrote:
Since August is the canonical time for vacation for many people it is
probably better to get into more concrete discussions in 3-4 weeks
from now, but people can already start thinking about their own areas
of responsibility concerning consolidation
Hi Alex,
> It works for me (tested with Isabelle2011) when I replace "null" with
> "List.null" (There is a hide_const (open) in List.thy). Otherwise the
> unfolding doesn't actually unfold anything :-)
You're right, it works, also with the latest Isabelle. I don't know what I
tested this morni
On Thu, 1 Sep 2011, Alexander Krauss wrote:
Here's an example. After "unfolding null_def", the user invoked
Sledgehammer and asked for an Isar proof. The "proof - ... qed" block after
that is generated by Sledgehammer:
lemma "null xs ==> tl xs = xs"
proof -
assume nx: "null
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;
>
On Fri, 2 Sep 2011, Christian Urban wrote:
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
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
The reason that this issue has just recently become apparent, is due to
changes 322d1657c40c ff. by Andreas Lochbihler. He assisted in replacing
(Stefan Berghofer's) SML code generator invocations by generic code
generator invocations to enable the long-term removal of the SML code
generator.
13 matches
Mail list logo
