Am 27/08/2012 13:35, schrieb Makarius:
> It is generally a good move to develop a habit to allocate some small amounts
> in
> project proposals etc. for "Poly/ML software maintenance" and direct it to
> David. This is how things can continue, and David gets a tiny little bit of
> recompense for h
Am 29/08/2012 14:21, schrieb Makarius:
> On Wed, 29 Aug 2012, Gerwin Klein wrote:
>
>> A small annoyance with document_output was that the output doesn't seem to
>> get
>> produced for document=false (i.e. seems to force a latex run) and that it
>> insists on creating a "document" subdirectory in
Am 29/08/2012 14:21, schrieb Makarius:
> On Wed, 29 Aug 2012, Gerwin Klein wrote:
>
>> A small annoyance with document_output was that the output doesn't seem to
>> get
>> produced for document=false (i.e. seems to force a latex run) and that it
>> insists on creating a "document" subdirectory in
Am 30/08/2012 22:37, schrieb Makarius:
> On Thu, 30 Aug 2012, Tobias Nipkow wrote:
>
>> I am still having some problems with it. Given
>>
>> session "HOL-IMP1" in "~~/src/HOL/IMP" = HOL +
>> options [document_output="IMP-generated", doc
Am 05/09/2012 15:46, schrieb Makarius:
> On Wed, 5 Sep 2012, Lars Noschinski wrote:
>
>> As far as I can see, the only way to issue a successful "show" after a wrong
>> assumption (or, if you prefer, an "assumption which does not fit any of the
>> pending goals") is discarding everything with "nex
Am 07/09/2012 16:51, schrieb Makarius:
> On Thu, 6 Sep 2012, Tobias Nipkow wrote:
>
>> Am 05/09/2012 15:46, schrieb Makarius:
>>> On Wed, 5 Sep 2012, Lars Noschinski wrote:
>>>
>>>> As far as I can see, the only way to issue a successful "show&q
Am 05/09/2012 14:45, schrieb Lars Noschinski:
> I like this goal; but, as you said, this is a long term process and a solution
> to this particular issue does not need more then a `peepwhole view`. We also
> don't deviate much from existing practice, as "show" does a similar trick
> already.
Let
When using jedit (development version) I got into the following situation:
partial proof
(* long
comment
*)
Because of the length of the comment (which was a lemma I had to comment out
because due to the partial proof above, proof methods in it diverged) the end of
the comment was outside the
Brilliant stuff, the improvemenst are dramatic (again)!
Tobias
Am 17/09/2012 15:44, schrieb Makarius:
> Poly/ML 5.5.0 has been released officially a few days ago. In
> Isabelle/a93d920707bb it is now included as one of the "main" components by
> default, so subscribers to the new component setup
That's very kind of him, assuming he was not the one who broke KBPs. This is
just another reminder that people should watch the AFP when they check in
changes, and fix them. The testboard runs most of the AFP.
Tobias
Am 21/09/2012 09:12, schrieb Lukas Bulwahn:
> Thanks to Dmitriy's effort, all AF
This is what you should not do: search and replace a string selectively that
occurs many times in a theory. I did this twice (the second time to see if it
was repeatable), using Replace & Find, and after about 50 replacements, jedit
went all funny and screwed up the window manager on my mac. Once I
For example 03bc7afe8814
Tobias
Am 02/10/2012 20:11, schrieb Makarius:
> On Tue, 2 Oct 2012, Tobias Nipkow wrote:
>
>> This is what you should not do: search and replace a string selectively that
>> occurs many times in a theory. I did this twice (the second time to see if it
I believe you need to do
isabelle components -a
and it will download all missing components. It's a really neat system.
Tobias
Am 04/10/2012 15:47, schrieb Lawrence Paulson:
> Does anybody understand the attached message, which seems to involve the new
> build system?
> Larry
>
> ~/isabelle/R
Am 16/10/2012 13:22, schrieb Tjark Weber:
> Hi,
>
> Class semiring in HOL/Rings.thy [1] assumes
>
> left_distrib: "(a + b) * c = a * c + b * c"
> right_distrib: "a * (b + c) = a * b + a * c"
>
> This is different from the terminology used in Wikipedia [2],
> MathWorld [3] and much of the lit
Am 17/10/2012 11:09, schrieb Makarius:
> *** ML ***
>
> * Type Seq.results and related operations support embedded error
> messages within lazy enumerations, and thus allow to provide
> informative errors in the absence of any usable results.
>
>
> *** General ***
>
> * More informative error m
In jedit, numerals of polymorphic type are no longer tagged with the type
variable as a warning. That is an extremely helpful warning not just for
beginners, it would be a pity to lose that in jedit.
Tobias
___
isabelle-dev mailing list
isabelle-...@in.t
Am 22/10/2012 14:16, schrieb Tjark Weber:
> On Sun, 2012-10-21 at 16:46 +0200, Florian Haftmann wrote:
>> Btw. whenever I'm testing the AFP these days without relying on the
>> testboard I use the following [...]
>
> In the last few months I've seen several emails with testing advice on
> this l
Am 27/10/2012 16:55, schrieb Makarius:
> On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote:
>
>> is there an implementation of priority queues in the isabelle library?
>
> This is off-topic for this mailing list, which is for things happening around
> the Isabelle development process. Unless you r
Am 27/10/2012 18:23, schrieb Makarius:
> On Sat, 27 Oct 2012, Tobias Nipkow wrote:
>
>> Am 27/10/2012 16:55, schrieb Makarius:
>>> On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote:
>>>
>>>> is there an implementation of priority queues in the isabelle l
Hi Christian,
I think we stumbled across the same problem (unless I am mistaken, in which case
Gerwin can tell you how we solved it).
This does not solve your problem but may still be of interest: In the
development version of the LaTeX Sugar manual, there is a description how to
create tex snipp
This is exactly why I am against SMT certificates in AFP entries. Ondrej, can
you possibly remove them?
Tobias
Am 08/11/2012 11:55, schrieb Jasmin Christian Blanchette:
> Hi Gerwin,
>
> Am 07.11.2012 um 22:41 schrieb Gerwin Klein:
>
>> *** Bad certificate cache: missing certificate
>> *** At co
Am 16/11/2012 14:47, schrieb Makarius:
> On Tue, 2 Oct 2012, Tobias Nipkow wrote:
>
>> This is what you should not do: search and replace a string selectively that
>> occurs many times in a theory. I did this twice (the second time to see if it
>> was repeatable), using R
Thanks for looking into it. I will upgrade to Montain Lion soon and will test it
myself again.
Tobias
Am 19/11/2012 17:10, schrieb Makarius:
> On Sun, 18 Nov 2012, Tobias Nipkow wrote:
>
>> Am 16/11/2012 14:47, schrieb Makarius:
>>> On Tue, 2 Oct 2012, Tobias Nipkow wrote:
Most of the theories in there are loaded via Library.thy. But a few are loaded
via ROOT. What is the rational for this subdivision? It looks like code
generation is the difference, but why?
Thanks
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.
For whom efficient code is a concern:
* Library/IArray.thy: immutable arrays with code generation.
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
I believe Gerwin already reported this in some email, and I can confirm it: the
afp test hangs even on my own laptop. The trace:
lapbroy100:AFP nipkow$ isabelle afp_build -A
Building Jinja ...
Finished Jinja (0:05:06 elapsed time, 0:15:28 cpu time, factor 3.03)
Building LatticeProperties ...
Finis
, schrieb Lars Noschinski:
> On 05.12.2012 08:31, Tobias Nipkow wrote:
>> I believe Gerwin already reported this in some email, and I can confirm it:
>> the
>> afp test hangs even on my own laptop. The trace:
>>
>> lapbroy100:AFP nipkow$ isabelle afp_build -A
>&g
Am 05/12/2012 16:46, schrieb Jasmin Christian Blanchette:
> Am 05.12.2012 um 16:33 schrieb Tobias Nipkow:
>
>> I tried again (but after some hg fetches, and am now on 3ae4376cb739), and
>> now
>> HOL still builds but HOLCF hangs. On the other hand Johannes (running Linux
Am 05/12/2012 22:50, schrieb Gerwin Klein:
> On 05/12/2012, at 6:31 PM, Tobias Nipkow wrote:
>
>> Can anybody still build the AFP on some machine?
>
> I have been able to build everything on a linux machine late last night.
>
> The only entry that comes up with an
Am 06/12/2012 12:57, schrieb Makarius:
> This does not say anything yet. We need to collect further details and
> hypotheses and test them. I will also try again to reproduce it myself.
One point may (or may not) have got lost. The problem seems to be independent
from the AFP. Remember that I ha
I'll look at it, thanks.
Tobias
Am 09/12/2012 12:50, schrieb Christian Sternagel:
> I fixed an error that only came up during document preparation (which I should
> have tested previously, sorry).
>
> cheers
>
> chris
>
> On 12/09/2012 02:27 PM, Christian Sternagel wrote:
>> Dear all,
>>
>> I
Am 10/12/2012 13:38, schrieb Makarius:
> On Fri, 30 Nov 2012, Lukas Bulwahn wrote:
>
>> It must be considered unmaintained. The benchmarks themself I will
>> irregularly
>> have time on weekends and nights to have a look, but I cannot keep up with
>> "Isabelle roaring ahead".
>
> After several w
I suspect many people will have experienced the same confusion, and Makarius
acknowledged this in some email when he spoke of the `joke' "build -b". Renaming
"build" would make sense.
Tobias
Am 12/12/2012 22:49, schrieb Jasmin Christian Blanchette:
> Hi all,
>
> The new "isabelle build" tool is
Am 13/12/2012 03:21, schrieb Alessandro Coglio:
> Hello,
>
> Is there a process to propose extensions to the Isabelle library? Is
> isabelle-dev the right place, as opposed to isabelle-users?
>
> As part of an Isabelle project, I've developed some type classes and theorems
> for orders and lattic
I tried to apply your patch but failed (see below). Since I had a problem with
somebody else's patch before, I wonder if something is wrong at my end? Any
suggestions?
Tobias
$ hg import emb
applying emb
patching file NEWS
Hunk #1 FAILED at 172
Hunk #2 FAILED at 181
2 out of 2 hunks FAILED -- sav
ame for sup, Inf, and Sup).
>
> On a semi-related topic, I was wondering why the Isabelle library has
> syntactic
> type classes for many (most?) operators but not for bot and top.
Florian can answer that one better than me.
Tobias
> Thanks!
>
>
>
> On 12/13/12
Am 17/12/2012 11:34, schrieb Makarius:
> On Sat, 15 Dec 2012, Florian Haftmann wrote:
>
>> Hi all,
>>
>>> The reason is that Open_Induction/ROOT (and also
>>> Open_Induction/Open_Induction.thy) relies on $AFP being set, which is
>>> only the case if AFP is registered as a component (which is not t
Am 21/12/2012 05:18, schrieb Christian Sternagel:
> Dear all,
>
> I suggest to add the following lemmas to Transitive_Closure and the simplifier
> (I just copied the unicode-tokens from Isabelle/jEdit... I hope what arrives
> after emailing is the same what I sent):
>
> lemma
> reflcl_idemp [si
I have just added a new theory Library/Finite_Lattice. It clashes with theory
Library/Countable in a way I don't understand. If you import both
theory Scratch
imports "~~/src/HOL/Library/Finite_Lattice" "~~/src/HOL/Library/Countable"
begin
Isabelle complains
Unproven class relation finite_lattic
Am 29/12/2012 19:59, schrieb Makarius:
>> 2) testing changes:
>> Before publication, pull any changes from the official repository. (This
>> might
>> effect a merge.) Now test your changes at least by
>>
>> isabelle build -a -o browser_info -o document=pdf -o document_graph
>
> This "-o documen
Am 01/01/2013 14:10, schrieb Makarius:
> On Sun, 30 Dec 2012, Tobias Nipkow wrote:
>
>>> The hints in README_REPOSITORY and the "system" manual suggest that
>>> "isabelle
>>> build -a" is the standard way to build all Isabelle sessions.
>&g
In principle a good idea, but I don't think we want multiple intros for
different audiences. Hence I would aim for a general intro that also covers
points that PG users are used to.
Tobias
Am 22/01/2013 13:30, schrieb Lawrence Paulson:
> Do we provide an introduction to Isabelle/jEdit for PG user
Am 15/02/2013 13:12, schrieb Makarius:
> On Do, 2013-02-14 at 17:22 +, Lawrence Paulson wrote:
>> In a dream scenario, one might imagine opening a document containing a number
>> of occurrences of "sorry", and each one of these occurrences would be given
>> to
>> counterexample finders and to
Am 15/02/2013 14:21, schrieb Jasmin Christian Blanchette:
> Am 15.02.2013 um 13:37 schrieb Tobias Nipkow :
>
>> Triggering s/h via "sorry" (or some other explicit means) is perfectly
>> reasonable, but having the IDE invoke s/h based on time outs and guesses
>>
Am 17/02/2013 19:41, schrieb Christian Urban:
>
>
> 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
>
Am 18/02/2013 15:10, schrieb Lawrence Paulson:
> These definitions originate in Isabelle/ZF, where it is quite essential to
> have a condition such as "r <= A <*> A", because otherwise no reflexive r
> could exist. They aren't is obviously necessary in Isabelle/HOL, but
> nevertheless the idea t
Am 19/02/2013 03:50, schrieb Christian Sternagel:
> On 02/18/2013 11:31 PM, Tobias Nipkow wrote:
>> Am 18/02/2013 15:10, schrieb Lawrence Paulson:
>>> These definitions originate in Isabelle/ZF, where it is quite essential to
>>> have a condition such as "r &
It would be better to update it. The German version is also a bit odd...
Tobias
Am 19/02/2013 00:42, schrieb Lawrence Paulson:
> Leaves something to be desired. Starting with the first sentence. Do we care?
>
> Larry
>
> http://en.wikipedia.org/wiki/Isabelle_(proof_assistant)
>
>
Load attached theory in HOL/IMP. Go to line
done (* exception *)
and you'll see the subject line.
I am on parent: 51188:9b5bf1a9a710 tip
Tobias
Abs_Int2_ivl2.thy
Description: application/extension-thy
___
isabelle-dev mailing list
isabelle-...@in.tum.
It is a fairly huge goal state that is supposed to get printed there. With all
the annotations, it may exceed the limit. But why is code generation involved at
that point ("done")?
Tobias
Am 21/02/2013 15:56, schrieb Makarius:
> On Thu, 21 Feb 2013, Tobias Nipkow wrote:
>
Now that I know that this is a resource limitation and not an error, I'm happy
again.
Thanks
Tobias
Am 21/02/2013 16:51, schrieb Makarius:
> On Thu, 21 Feb 2013, Tobias Nipkow wrote:
>
>> It is a fairly huge goal state that is supposed to get printed there. With
>> all
Am 26/02/2013 17:17, schrieb Lawrence Paulson:
> A student has forwarded this problem to me. It seems weird and unbelievable.
> What have I overlooked?
>
> I tidied it up slightly (see below) but I get the same error message.
>
> lemma "True"
> proof -
> have "True = (∃x. (λy. True) x)"
that the type of X may also be to blame.
Yes, your lambda y is actually a distraction.
Tobias
> Larry
>
> On 26 Feb 2013, at 16:27, Tobias Nipkow wrote:
>
>> The two y's are given separate types. In fact, Isabelle introduces ??'a
>> itself
>> in th
Am 27/02/2013 15:28, schrieb Makarius:
> On Wed, 27 Feb 2013, Lawrence Paulson wrote:
>
>> A behaviour where "..." denotes something other than the previous right-hand
>> side needs to be fixed.
>
> Again this odd "bug -- fixed" terminology. Such problems are much deeper.
>
> Fortunately, the
Am 27/02/2013 16:44, schrieb Makarius:
> On Wed, 27 Feb 2013, Tobias Nipkow wrote:
>
>> definition my0 :: nat where "my0 = length []"
>>
>> into a definition of a constant of type "'a itself ⇒ nat" with an additional
>> parameter. Although
Am 16/03/2013 01:29, schrieb Lawrence Paulson:
> At d5c95b55f849
>
>> ~/isabelle/Repos/src/HOL: isabelle components -a
>> ### Missing Isabelle component:
>> "/Users/lp15/.isabelle/contrib/jedit_build-20130104"
>> Getting "http://isabelle.in.tum.de/components/jedit_build-20130104.tar.gz";
>> Unpac
Am 29/03/2013 11:24, schrieb Makarius:
> On Thu, 28 Mar 2013, Manuel Eberl wrote:
>
>> I just noticed that when exporting code to Haskell, there is a complication
>> when some of the theories involved have lower-case names. The code export
>> itself will work with no error or warning, but when ghc
Holger Gast has ben added to the Unix group isabelle, if that is what you mean.
He is a member of my chair for half a year, that is why, similar to all other
members of the chair.
Tobias
Am 12/04/2013 13:08, schrieb Makarius:
> This needs to be a broadcast, because there is no additional informat
Am 12/04/2013 13:59, schrieb Makarius:
> On Fri, 12 Apr 2013, Tobias Nipkow wrote:
>
>> Holger Gast has ben added to the Unix group isabelle, if that is what you
>> mean. He is a member of my chair for half a year, that is why, similar to all
>> other members of the chai
Let me just make some remarks as a user. At ITP 2011 I published a paper
http://www21.in.tum.de/~nipkow/pubs/itp11.html where I showed how to use locales
to structure stepwise development of modules (see p11). In that context I
intentionally used the notation
interpretation (in A) B-expr
instead
I was under the impression that type synonyms are expanded in typ
antiquotations, but apparently not, at least not with 30624dab6054. If I write
@{typ vname} I get "vname", even if vname is a type synonym for string. Maybe it
has always been like this, but it means that one cannot automatically dis
Am 27/05/2013 19:54, schrieb Makarius:
> On Mon, 27 May 2013, Makarius wrote:
>
>> The change ensures that variables with equal name are unified, in the same
>> manner as the types of Free or Const are unified, before doing the real work
>> of HO-unification.
>
> Here is another example for Isabe
Am 27/05/2013 18:13, schrieb Makarius:
> On Mon, 27 May 2013, Stefan Berghofer wrote:
>
>> As I pointed out in my previous mail, it is an error to supply disagreement
>> pairs to unify containing Vars that have the same name but different types.
>> So
>> I don't think one should change pattern.ML
Am 28/05/2013 13:34, schrieb Lawrence Paulson:
> Historical note: when the original high-order unification code was written,
> there was no user-level polymorphism. If my memory is correct, the TVar
> constructor did not even exist. Polymorphism was only used for type inference
> in terms.
corr
Am 28/05/2013 20:52, schrieb Makarius:
> On Tue, 28 May 2013, Lawrence Paulson wrote:
>
>> the disagreement pairs should be fully eta-expanded by this point
>
> I've spent further thoughts on that: somehow it increases my uneasyness, since
> it looks like the full type information needs to be kno
Am 28/05/2013 23:53, schrieb Makarius:
> On Tue, 28 May 2013, Tobias Nipkow wrote:
>
>> Am 28/05/2013 13:34, schrieb Lawrence Paulson:
>>> Historical note: when the original high-order unification code was written,
>>> there was no user-level polymorphism. If
this incident has again reminded me that in the absence of formal proofs about
the code, assertions in the code would be a big step forward. they could have
told us a long time ago that some precondition expected by the unification code
is not guaranteed. lukas and a student had even put together a
on of an unstated
precondition. So in addition to verifying the unification code you have to
verify all calls of it.
Assertions/testing and verification are complementary, with very different costs
and benefits.
Tobias
Am 30/05/2013 11:50, schrieb Makarius:
> On Thu, 30 May 2013, Tobias Nipk
Am 30/05/2013 13:41, schrieb Lawrence Paulson:
> The only question is whether Isabelle is important enough for such work to be
> seen as significant in a wider context.
Makarius is right, the interaction of schematic type variables and HOU has never
been nailed down properly and would be of inter
Am 30/05/2013 13:49, schrieb Tobias Nipkow:
> Am 30/05/2013 13:41, schrieb Lawrence Paulson:
>> The only question is whether Isabelle is important enough for such work to
>> be seen as significant in a wider context.
>
> Makarius is right, the interaction of schematic type
ry
>
> On 30 May 2013, at 13:04, Tobias Nipkow wrote:
>
>>
>> Am 30/05/2013 13:49, schrieb Tobias Nipkow:
>>> Am 30/05/2013 13:41, schrieb Lawrence Paulson:
>>>> The only question is whether Isabelle is important enough for such work to
>>>>
in case "u" contains further
synonyms). This is getting a bit too fine grained.
This may be one of the rationals why @{typ} works the way it does.
Tobias
Am 21/05/2013 13:49, schrieb Makarius:
> On Thu, 18 Apr 2013, Tobias Nipkow wrote:
>
>> I was under the impress
It is best to communicate such changes to theories directly to the author of the
theory. Or enquire on isabelle-users who feels responsible for that theory to
get in touch with him. I guess your email is an instance of the "who feels
responsible" and Johannes will take care of it.
Thanks
Tobias
A
Am 05/07/2013 14:08, schrieb Makarius:
> On Tue, 2 Jul 2013, Gerwin Klein wrote:
>
>> I'm less sure about the distinction between sub and sup. I can see it mostly
>> aligns with current usage patterns, but I find this distinction even more
>> confusing.
>
> There are two aspects here: (1) common
Am 10/07/2013 16:54, schrieb Makarius:
> That is an instance of \<^sup>LETTER, i.e. the remaining overlap from the
> earlier discussion on this thread. I have presently escaped the situation by
> using \<^bsup> \<^esup> which looks almost the same in Latex, but is a bit
> awkward in Isabelle/jEdit
Am 18/07/2013 22:44, schrieb Makarius:
> On Thu, 18 Jul 2013, Florian Haftmann wrote:
>
> "Code generator: dropping subsumed code equation" by Auto Quickcheck
> I guess it would be the task the tools to omit such outbursts and not
> globally on the IDE side?
In principle
I suspect that the csdp server may be unreachable at times.
Tobias
Am 08/08/2013 14:37, schrieb Makarius:
> On Thu, 8 Aug 2013, Gerwin Klein wrote:
>
>> Tobias and I just tried from a laptop on version 41ebc19276ea, which seems to
>> work fine. Has somebody fixed it in the meantime?
>
> I did n
Am 17/08/2013 15:20, schrieb Makarius:
> On Thu, 15 Aug 2013, Lawrence Paulson wrote:
>
>> I think that the only way to achieve the documented behaviour is to replace
>> all schematic variables in the goal by Frees before attempting resolution.
Which can be done safely outside the kernel.
> If y
Am 17/08/2013 15:24, schrieb Makarius:
> On Thu, 15 Aug 2013, Lawrence Paulson wrote:
>
>> On 13 Aug 2013, at 10:35, Lars Noschinski wrote:
>>>
>>> It might be interesting to note that also Unify.matchers is not able to
>>> match
>>> such term.
>
> This old thread on Unify.matchers might be als
ecialist tools.
That's what I meant. It should merely state explicitly that "these tactics
merely discard unifiers that would update the goal state." can lead to
incompleteness.
Tobias
> Larry
>
> On 19 Aug 2013, at 07:11, Tobias Nipkow wrote:
>
>> Am 17/08/20
When you clicked on the proof generated by sledgehammer in jedit, it would
replace the sledgehammer call in the theory text with the proof, which was
*very* convenient. Alas, that has gone away recently (eg 9228c575d67d). I don't
know if it was intentional or not, the NEWS file does not seem to men
Please disregard my previous email. I see that there is now a sledeghammer panel
(with some more goodies) which avoids having to type sle... and thus solves the
issue.
Thanks for that
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://ma
Am 02/09/2013 11:18, schrieb Makarius:
> The sledgehammer panel has had only 1-2 rounds of refinements so far, and more
> precise observations by testers on this mailing list will be required to make
> it
> work smoothly for the coming release.
>
Some observations:
- When clicking on the genera
, because these
> calls are often quite lengthy text strings.
>
> Larry
>
> On 2 Sep 2013, at 11:31, Tobias Nipkow wrote:
>
>> - Sometimes I click on the generated proof and it is not pasted into the
>> theory
>> text. It just doesn't work, even if I c
For uniformity I almost always use "=" and would not like to see it printed as
<-->.
Tobias
Am 02/09/2013 16:24, schrieb Makarius:
> (This is just a side-track on HOL notation, which came to me when cleaning up
> theories with old ASCII replacement syntax like & | --> <-> Un Int etc. --
> which
The earlier the better because, as I told you at ITP, I have a course starting
in the middle of October and they need to use a new Isabelle, in the worst case
a release candidate.
Tobias
Am 02/09/2013 15:37, schrieb Makarius:
> The French summer vacation period has ended, so I've switched myself
You mean parentheses, not braces. This is an intentional change. See the NEWS:
* Weaker precendence of syntax for big intersection and union on sets,
in accordance with corresponding lattice operations. INCOMPATIBILITY.
Tobias
Am 11/09/2013 11:31, schrieb C. Diekmann:
> Hi,
>
> I just downloa
It worked for me this morning.
Tobias
Am 17/09/2013 12:28, schrieb Lars Hupel:
> I was trying to update to the repository version today, but:
>
> $ bin/isabelle components -a
> ### Missing Isabelle component: "/home/lars/.isabelle/contrib/jdk-7u40"
> Getting "http://isabelle.in.tum.de/components
I just noticed the following behaviour in 705f0b728b1b: When the cursor remains
fixed in the theory window and I scroll in that window with the help of the
scoll bar, the output window goes blank when the line with the cursor is no
longer visible. I have no idea when that changed but in Isabelle 20
Am 18/09/2013 17:38, schrieb Makarius:
> On Wed, 18 Sep 2013, Tobias Nipkow wrote:
>
>> When the cursor remains fixed in the theory window and I scroll in that
>> window
>> with the help of the scoll bar, the output window goes blank when the line
>> with the curso
For users of the development version of the AFP only:
Native Word
Andreas Lochbihler
This entry makes machine words and machine arithmetic available for code
generation from Isabelle/HOL. It provides a common abstraction that hides the
differences between the different target languages. The cod
Am 21/09/2013 03:08, schrieb Alessandro Coglio:
> Hello,
>
> The attached file contains a fairly heterogeneous collection of potential
> extensions to the Isabelle library, which I've been developing as part of some
> projects that I'm working on. I think that other Isabelle users may find them
>
Am 21/09/2013 03:08, schrieb Alessandro Coglio:
>
> I also have a general question about library vs. AFP. There seem to be clear
> cases of things that should go into the library (e.g. new theorems on lists or
> sets) and clear cases of things that should go into the AFP (e.g. a theory of
> conte
Am 30/09/2013 12:45, schrieb Makarius:
> In preparation of Isabelle2013-1 the Isabelle website needs the usual updating
> and polishing.
>
> The relevant repository is here:
> https://bitbucket.org/isabelle_project/isabelle-website/
>
> Traditionally my main job is to get the Download / Install
With Isabelle/jedit (566b769c3477) I get
"remote_vampire": Error: SystemOnTPTP is currently not available: ERROR: Cannot
make temp dir /tmp/SystemOnTPTPFormReply634.
"remote_e_sine": Error: SystemOnTPTP is currently not available: ERROR: Cannot
make temp dir /tmp/SystemOnTPTPFormReply634.
It loo
Thank you for this, Florian. The one thing I had hoped for when I initiated
this change was that one can write "n-1" just like "n+1", but that doesn't
quite work yet, probably because you have some special syntax for what used to
be negative numerals. This may ease the conversion, but can we get ri
Am 20/11/2013 22:49, schrieb Makarius:
> Are there any other potential problems of Isabelle2013-1 that were not
> reported
> yet?
There is a problem with autoquickcheck in Isabelle/jedit. It sometimes fails to
find or dislay a counterexample. I have a theory with a wrong lemma in it. When
I load
achine is loaded by proving the theory, quickcheck times out.
> After the edit, there is less load, and quickcheck is faster.
>
> --
> Peter
>
>
> On Do, 2013-11-21 at 10:40 +0100, Tobias Nipkow wrote:
>> Am 20/11/2013 22:49, schrieb Makarius:
>>> Are there a
It says Timeout. Presumably this supports your guess.
Tobias
Am 21/11/2013 15:34, schrieb Makarius:
> On Thu, 21 Nov 2013, Tobias Nipkow wrote:
>
>> Some such effects may indeed play a role, although I originally did not
>> observe
>> it when reloading a theory but w
I just saw the above message for the first time, when building HOL-IMP. Should
this worry me?
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
201 - 300 of 464 matches
Mail list logo
