One could argue that sets are the canonical indexing structure. On the other
hand, we have syntax to make the actual names irrelevant.
Larry
On 24 Sep 2014, at 11:18, Johannes Hölzl hoe...@in.tum.de wrote:
Why Sum and not Sum_set in c)? Is the intention that the canonical type
always gets
It is also my experience that the server is extremely slow.
Larry
On 22 Sep 2014, at 15:52, Makarius makar...@sketis.net wrote:
On Thu, 11 Sep 2014, Lawrence Paulson wrote:
I have installed a copy of the software locally. Would be worth making this
a component?
This canonical question
A gain in legibility for sure.
Larry
On 18 Sep 2014, at 15:11, Tobias Nipkow nip...@in.tum.de wrote:
On 18/09/2014 15:47, Florian Haftmann wrote:
Changeset #fe083c681ed8 introduces products over lists. There has been
some private discussion whether there could be a serious attempt to
I have installed a copy of the software locally. Would be worth making this a
component?
--lcp
On 11 Sep 2014, at 13:07, Tobias Nipkow nip...@in.tum.de wrote:
On 11/09/2014 14:05, Jasmin Christian Blanchette wrote:
Hi all,
It appears that the Sum of Squares server is down. This
I’m afraid that I don’t even know what it is.
Larry
On 11 Jul 2014, at 12:21, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken
has not been addressed since before the last release.
So, which path to
Strange — I took a look (with the latest versions, same ids as quoted) and it
was fine.
On 18 Jun 2014, at 18:47, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
isabelle: 88263522c31e tip
afp: b514f0bac50e tip
Completeness FAILED
*** Failed to load theory Soundness
I certainly agree with your point of view, but I would immediately insert the
local context around any proof that causes problems rather than waste time
trying to fix it.
Maybe we could then invite the maintainers of the entries to update their
proofs if they wish.
Larry
On 5 Jun 2014, at
Didn’t we agree that a “backward compatibility mode” declaration (restoring the
former behaviour) would have to be available? That should make repairing legacy
proofs trivial. Naturally we would like to gradually port some of these
developments to do things the new way, but only some of them,
What new users see when they look at the actual definition of lists is not that
important. There are many, many situations where the actual definition of
something is much more complicated than the idealised version that one would
use for teaching. What is necessary is that simple-looking
it’s not just about syntactic sugar. It seems to me that the complex numbers
are an elegant (if degenerative) example of a co-algebraic datatype. The
co-recursive definitions look absolutely natural to me.
Larry
On 11 May 2014, at 12:55, Andrei Popescu uuo...@yahoo.com wrote:
The fact that
I used it a little bit last night, and couldn't notice any differences.
--lcp
On 17 Apr 2014, at 14:59, Makarius makar...@sketis.net wrote:
On Wed, 16 Apr 2014, Makarius wrote:
Since the jdk-8 zero release from a few weeks ago work generally well on
all platforms, I have now updated the
I am trying to understand why all four of these appear to be independent
theorems even though the “greater than” relations are nothing but
abbreviations. And maybe the problem is here:
abbreviation (input)
greater_eq (infix = 50) where
x = y ≡ y = x
abbreviation (input)
greater
PIDE does an awful lot already, and I’d worry about burdening it with yet more
functions.
It’s easy to get PDF from HTML, provided the quality is high enough. The other
direction does not work.
Larry
On 15 Apr 2014, at 09:51, Christian Sternagel c.sterna...@gmail.com wrote:
On 04/14/2014
Looks nice. Just the indenting needs fixing.
Larry
On 12 Apr 2014, at 11:58, John Wickerson johnwicker...@cantab.net wrote:
Hi all,
I've been thinking about and playing with the theory to HTML feature of
Isabelle. The PDF output is handy for producing papers, but I do find HTML so
much
On 12 Apr 2014, at 17:01, Lawrence Paulson l...@cam.ac.uk wrote:
Looks nice. Just the indenting needs fixing.
Larry
On 12 Apr 2014, at 11:58, John Wickerson johnwicker...@cantab.net wrote:
Hi all,
I've been thinking about and playing with the theory to HTML feature of
Isabelle
The theory Fields.thy declares the following simprules:
lemma divide_minus_left [simp]: (-a) / b = - (a / b)
lemma divide_minus_right [simp]: a / - b = - (a / b)”
The idea is that extracting the minus sign yields a good normal form. But it
seems that sometimes this works in the opposite
A very good idea, which reduces the impact of the change on existing proofs. I
am trying it out now.
Seeing no objections, I am quite likely to push this change later today.
Larry
On 4 Apr 2014, at 15:08, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
lemma
I wasn’t aware of this detail. But for people who use field_simps explicitly,
it neutralises the effect of removing those two as default simprules.
Larry
On 4 Apr 2014, at 17:09, Tobias Nipkow nip...@in.tum.de wrote:
Florian, can you give an example where previously
field_simps was too weak
I don’t think this is worth doing.
However some sort of process of identifying and cleaning up horrible old proofs
might be worth considering.
Larry
On 18 Mar 2014, at 21:23, Makarius makar...@sketis.net wrote:
Maybe I should try to improve the implicit rule method to reveal the rule
that
I may partly be to blame by introducing some metis calls. But there are some
terrible proofs here (e.g. just “rule”, WTF?).
Larry
On 18 Mar 2014, at 20:58, Brian Huffman huffman.bria...@gmail.com wrote:
On Tue, Mar 18, 2014 at 12:55 PM, Makarius makar...@sketis.net wrote:
Are you actually
But working very well, in my experience.
Now, will smt2 calls be suitable for the Library and AFP?
Larry
On 6 Mar 2014, at 15:43, Jasmin Christian Blanchette
jasmin.blanche...@gmail.com wrote:
As you may know, Sascha and I have been working on a new version of the smt
proof method, called
...@gmail.com wrote:
Am 13.02.2014 um 13:19 schrieb Lawrence Paulson l...@cam.ac.uk:
I’m not sure what the question is any more. If it is about the choice of
names in Skolemization, that has been entirely redone in the past few years.
I imagine it is now something like
I wonder if it could somehow be wiki driven, so that people could edit it
themselves?
Larry
On 24 Jan 2014, at 12:17, Makarius makar...@sketis.net wrote:
On Mon, 20 Jan 2014, Christian Sternagel wrote:
I am back from JAIST (in Japan) to the University of Innsbruck again. Could
you please
It is impressive first-year geographical reach, if not for absolute numbers.
What about a fully automatic system based on analysis of web server logs?
Yet another approach: to associate the world map with the AFP, with a pin at
every address from which an AFP entry has been accepted (whether
Great news! I hope to see a brief announcement paper illustrating some of the
new things that can be done. Or did you publish that last year?
Larry
On 21 Jan 2014, at 12:54, Jasmin Christian Blanchette
jasmin.blanche...@gmail.com wrote:
*** HOL ***
* Moved new (co)datatype package and its
The name makes sense: thin refers to deleting the assumption.
It is ugly of course, which will be an incentive for users to update their
proofs.
Larry
On 15 Jan 2014, at 15:05, Makarius makar...@sketis.net wrote:
On Tue, 14 Jan 2014, Thomas Sewell wrote:
If there is some collection of
This sounds great! You seem to have done everything right.
Having the compatibility mode will make it easy to get everything working again
quickly, with the conversion to the new setup becoming a background task
(possibly to be combined with refactoring horrible old proofs).
Larry
On 14 Jan
I think the problem is that the unsafe situations cannot be detected locally,
i.e., there is no way for the tactic to know that a particular free variable is
actually a locale constant. I could be wrong: the current treatment of contexts
may make this information available after all. That would
I’m impressed with your determination to slog through so many changes, but I am
not sure that we have the right to impose this on our users, which is why I
would prefer one of the other solutions, namely (1) contextual information if
available (2) some sort of compatibility mode.
Thank you
Note that this change would affect auto, force, fast, etc.
Possibly a “legacy” version of auto would help with compatibility, or otherwise
some sort of option setting to (locally) restore the old behaviour in all
affected methods.
Larry
On 13 Jan 2014, at 15:47, Makarius makar...@sketis.net
to
handling this sort of example.
Larry
On 7 Jan 2014, at 23:32, Makarius makar...@sketis.net wrote:
On Tue, 31 Dec 2013, Lawrence Paulson wrote:
(1) Do we need a general way to prevent warnings from breaking interfaces?
That would be great, if possible, and maybe just requires inserting some
There are two questions here:
(1) Do we need a general way to prevent warnings from breaking interfaces?
That would be great, if possible, and maybe just requires inserting some
sort of pause between messages to allow their interruption, or some way to
count messages and stop them after a
I’ve had a quick look, and it seems impressive. Better than MacHg, which also
appears no longer to be developed.
Larry
On 18 Dec 2013, at 19:25, Makarius makar...@sketis.net wrote:
Since I am presently on travel and only briefly looking through pending
mails, here is a publicized version of
Of course we don’t have any formal curation policy for the library, but Zorn's
lemma is a fundamental result. Perhaps we need to think about what things are
and are not allowed in the library. Deleting things will always be risky.
Larry
On 26 Nov 2013, at 11:30, Johannes Hölzl hoe...@in.tum.de
I doubt very much that many people are still using PG.
This wasn’t noticed because there was nothing to notice: the problem is the
absence of something, rather than the presence, so it’s subtle and insidious.
People may have encountered this problem without realising it.
Larry
On 21 Nov 2013,
Sounds good to me!
Larry
On 18 Nov 2013, at 17:58, Jasmin Christian Blanchette
jasmin.blanche...@gmail.com wrote:
Still, I want to make sure there is wide agreement before proceeding.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Sorry 7cec5a4d5532
Deleting Isabelle/lib/classes did the trick.
Larry
On 25 Sep 2013, at 14:58, Makarius makar...@sketis.net wrote:
I don't see a public Isabelle version of that id -- isn't that your project
repository?
Maybe your Isabelle clone got messed up locally, as a bad merge
/h
terminates.
Larry
On 24 Sep 2013, at 20:52, Makarius makar...@sketis.net wrote:
On Mon, 16 Sep 2013, Lawrence Paulson wrote:
Any generated metis calls only self-insert if clicked before s/h
terminates. If you ignore your session for a few minutes while s/h runs (as
many people do
Never tried using this with jEdit.
I won't mind having the Mac cursor-movement keyboard shortcuts.
Larry
On 24 Sep 2013, at 22:43, Makarius makar...@sketis.net wrote:
How important is the canonical key sequence COMMAND comma as defined by
Apple?
Some of the results in subsection {* Sets *} may be interesting. But your
product distribution laws are subsumed by the Sigma_XX_distrib{1,2} laws in
Product_Type.thy.
As for indexed products, check the existing HOL/Library/FuncSet.thy for
possible overlaps.
Larry
On 21 Sep 2013, at 03:08,
We also have some overlap between Library/Binomial and
Number_Theory/Binomial.
--lcp
On 19 Sep 2013, at 19:05, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Since, there 92080294beb8 are two clone theories:
Library/Univ_Poly.thy
Happened to me too. I deleted the component manually and retried.
--lcp
On 17 Sep 2013, at 11:28, Lars Hupel hu...@in.tum.de wrote:
I was trying to update to the repository version today, but:
$ bin/isabelle components -a
### Missing Isabelle component:
That fixed it.
Larry
On 13 Sep 2013, at 10:15, Jasmin Blanchette jasmin.blanche...@gmail.com wrote:
Just to make sure it's not MaSh-related somehow, I would also recommend you
comment out MASH=yes in your settings file and see if this has any impact.
Provers don't launch at all (according to process monitor) and no output,
either in the new S/H panel or via the sledgehammer command. I'm using
9d8764624487 but I don't think the precise version matters, as I grabbed a new
copy this morning and nothing's changed.
Anybody else seen this?
For sure. I think it confuses beginners at first, because == is only allowed in
real definitions rather than derived ones.
Larry
On 3 Sep 2013, at 00:39, Gerwin Klein gerwin.kl...@nicta.com.au wrote:
I also still use == quite a bit, I never understood why it is discouraged so
much. It has
I have also noticed the first issue you mention.
Regarding your other points, a) seems logical to me (you have made your
choice), while b) possibly simplifies the implementation significantly
(otherwise you need to remember to replace the previous choice rather than to
append the text), and it
To me, the ability to use = (on booleans) as an alternative to - is an
artefact of HOL, rather than something to encourage. Almost always, - is more
readable. At least that's my view.
Larry
On 2 Sep 2013, at 19:42, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Are there
It doesn't always work in the panel either. Some lurking bugs maybe. I'm not
sure what you are allowed to do while sh is running.
Larry
On 31 Aug 2013, at 09:04, Tobias Nipkow nip...@in.tum.de wrote:
Please disregard my previous email. I see that there is now a sledeghammer
panel
(with some
The main avenue for support is the users' mailing list, which is
isabelle-us...@cl.cam.ac.uk. You have mailed the developers' list.
I do suggest that you frame your question to include more technical detail,
because as things stand it's impossible to imagine what you are trying to do.
Larry
This is a tricky point, but on balance, I think it's better to have complete
documentation even if it draws people's attention to things they should
overlook.
Larry
On 19 Aug 2013, at 22:41, Makarius makar...@sketis.net wrote:
Of course you are welcome to update your documentation snippet
specialist tools.
Larry
On 19 Aug 2013, at 07:11, Tobias Nipkow nip...@in.tum.de wrote:
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
2013, at 12:30, Tobias Nipkow nip...@in.tum.de wrote:
Am 19/08/2013 12:45, schrieb Lawrence Paulson:
Your point of view makes sense on general principles, but not in this
particular case.
I had actually forgotten that these tactics existed. But they form a core
part of the classical
Probably you are right.
Larry
On 17 Aug 2013, at 14:20, Makarius makar...@sketis.net wrote:
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
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. I'm not
sure what effect this would have on performance.
Larry
On 13 Aug 2013, at 10:35, Lars Noschinski nosch...@in.tum.de wrote:
On
This could be a valuable service, especially for long lists of applys. (A proof
like by (induct n) auto should be left alone.)
Do ask an experienced user to examine your early attempts for beginner's
mistakes, like labelling all intermediate results.
Larry
On 30 Jul 2013, at 18:40, Josh
For sure, nested function variables like P (B x) are much too risky to use with
automation. It's essential, at the very least, to ensure that P is some
definite abstraction.
Larry
On 27 Jun 2013, at 12:00, Makarius makar...@sketis.net wrote:
On Thu, 27 Jun 2013, Makarius wrote:
This is a
, 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 interest to a larger
On 28 May 2013, at 19:52, Makarius makar...@sketis.net wrote:
... you do type unification of Free/Const/Bound incrementally as you go. So
some ?x::'?a could become a function indirectly, e.g. by unifying c::'?a with
c::nat=bool elsewhere.
This is never done, as far as I know. It is known
Description: Binary data
On 29 May 2013, at 10:25, Makarius makar...@sketis.net wrote:
On Tue, 28 May 2013, Lawrence Paulson wrote:
It clearly isn't a hardware failure. For one thing, it happens in the same
way on two separate machines, and anyway, a hardware failure wouldn't affect
only one
an earlier creation date from the other poly/ML
libraries.
Larry
On 29 May 2013, at 14:18, Makarius makar...@sketis.net wrote:
On Wed, 29 May 2013, Lawrence Paulson wrote:
I have just taken a look at the crash logs, and it's clear that some dynamic
libraries from a previous installation had got
. This is a source of incompleteness, but it has
always been there.
Larry
On 28 May 2013, at 13:11, Makarius makar...@sketis.net wrote:
On Tue, 28 May 2013, Lawrence Paulson wrote:
Historical note: when the original high-order unification code was written,
there was no user-level polymorphism. If my
I am glad to have PG (version 4.2) as an alternative for those occasions when I
get persistent bus errors with my theories using Isabelle/jEdit.
Larry
On 28 May 2013, at 16:41, Makarius makar...@sketis.net wrote:
See d3ee6315ca22, which is just a pro-forma update of the Isabelle component,
the disagreement pairs should be fully eta-expanded by this point, though I
haven't looked at the code recently. That would imply that the body_type cannot
be a function type.
Larry
On 28 May 2013, at 16:11, Makarius makar...@sketis.net wrote:
On Tue, 28 May 2013, Lawrence Paulson wrote
As I've said, these are poly/ML bus errors. My impression is that they arise
when Isabelle/jEdit is processing material under development, containing errors
and sledgehammer calls.
Larry
On 28 May 2013, at 17:45, Makarius makar...@sketis.net wrote:
Bus errors of the JVM (not Isabelle/jEdit!)
Naturally this notation is less important than before, and never strictly
essential. But would we save much by eliminating it?
Larry
On 21 May 2013, at 11:46, Makarius makar...@sketis.net wrote:
Does it mean you propose to discontinue (in a) at some point?
An old idea on my list is to add
Just had a crash on my (Mac) laptop too.
Larry
On 12 May 2013, at 12:24, David Matthews d...@prolingua.co.uk wrote:
On 11/05/2013 12:21, Tjark Weber wrote:
On Thu, 2013-05-02 at 16:18 +0100, Lawrence Paulson wrote:
I am getting a lot of poly/ML segmentation faults, and they are making
I am getting a lot of poly/ML segmentation faults, and they are making it very
difficult to do my work, especially as my theories take at least 15 minutes to
load. If it then simply crashes then I'm not getting anywhere.
Has anybody else had this problem with Poly/ML?
~/isabelle/Repos/src/HOL:
Stylesheets are about style, but the page also seems to have missing elements.
Is there a default stylesheet that we could take as a starting point?
Larry
On 21 Apr 2013, at 01:13, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Hi all,
what appears to me as the official
Some sort of visual indication that the same variable is being bound twice
might be useful, though that sort of thing is easy to overlook.
Larry
On 22 Mar 2013, at 13:15, Tjark Weber webe...@in.tum.de wrote:
On Fri, 2013-03-22 at 13:25 +0100, Makarius wrote:
On Fri, 22 Mar 2013, Andreas
I am getting quite a few Isabelle/jEdit crashes (with core dumps), at least one
a day.
Is there any point filing bug reports? The website for this looked a bit
formidable.
Larry
___
isabelle-dev mailing list
isabelle-...@in.tum.de
, Lawrence Paulson l...@cam.ac.uk wrote:
I've checked on another computer, and I get exactly the same thing.
File creation dates set in the past can cause a lot of problems, so it would
be interesting to know what is going on here.
Larry
Screen Shot 2013-03-18 at 11.44.38.png
On 18 Mar 2013
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;
Unpacking /Users/lp15/.isabelle/contrib/jedit_build-20130104.tar.gz
I agree with you, and it seems a mistake to expect jEdit to do all kinds of
things that could very easily be done otherwise.
Larry
On 14 Mar 2013, at 07:57, David Greenaway david.greena...@nicta.com.au wrote:
On 08/03/13 23:46, Joachim Breitner wrote:
Sometimes, when I’m writing
I can also imagine a use for this sort of thing. I use structured proofs when I
can, but in some situations it really isn't possible.
Larry
On 11 Mar 2013, at 16:51, Makarius makar...@sketis.net wrote:
This looks just like making the meaning of indentation a bit more formal.
Lets say as a
In Edinburgh LCF, term quotations containing anonymous type variables were
simply rejected. Perhaps that would still be the best approach now. I'm not
convinced that it would lead to more errors than the 'a itself approach.
Larry
On 1 Mar 2013, at 11:35, Makarius makar...@sketis.net wrote:
I
a version that
comes somewhere after the split with one somewhere before the split (via
plain diff), but how often does that happen? Isn't the typical use-case
comparison of successive changesets?
cheers
chris
On 02/27/2013 08:49 PM, Lawrence Paulson wrote:
I don't see the point
I don't see the point of splitting Zorn into multiple files. It isn't
especially large. Such a change really has nothing to do with the question of
locating proved results, and it would make it harder to examine past versions.
Larry
On 27 Feb 2013, at 05:57, Christian Sternagel
On 27 Feb 2013, at 12:23, Makarius makar...@sketis.net wrote:
On Tue, 26 Feb 2013, Lawrence Paulson wrote:
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
solution is
possible in this situation (calculations). To me it hardly differs from Fails
to refine any pending goal, and it should be treated similarly.
Larry
On 27 Feb 2013, at 14:28, Makarius makar...@sketis.net wrote:
On Wed, 27 Feb 2013, Lawrence Paulson wrote:
A behaviour where ... denotes
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) by simp
also have ... = (∃x. (λy. True) x)
oops
Larry
Begin
That mysterious type always throws me.
I guess you are saying that this dangling type dependence introduces a function
type in the first line. Unfortunately, this is a difficult matter to explain to
a student. I'll just have to tell him to constrain the types of his bound
variables. I believe
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)
___
isabelle-dev mailing list
isabelle-...@in.tum.de
It depends upon whether you regard having a carrier set as the norm or an
exception. I think there are many natural constructions on relations that can
only be done in the presence of a carrier set.
Larry
On 19 Feb 2013, at 02:50, Christian Sternagel c.sterna...@gmail.com wrote:
My main
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 that the domain type can be identified with the actual
Leaves something to be desired. Starting with the first sentence. Do we care?
Larry
http://en.wikipedia.org/wiki/Isabelle_(proof_assistant)
___
isabelle-dev mailing list
isabelle-...@in.tum.de
with the sledgehammer
execution.
Larry
On 14 Feb 2013, at 17:34, Peter Lammich lamm...@in.tum.de wrote:
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
...@gmail.com wrote:
Please consult the attached file for a first suggestion for the overview
page. (Just to make sure that I'm on the right track; if so I will continue
tomorrow ... today my wife won't allow ;); comments are most welcome.)
cheers
chris
On 01/25/2013 09:21 PM, Lawrence Paulson
it work in Proof
General? And the idea of having a whole bunch of gaps checked (as it were)
simultaneously is very appealing.
Larry
On 14 Feb 2013, at 12:58, Makarius makar...@sketis.net wrote:
On Thu, 14 Feb 2013, Lawrence Paulson wrote:
The entire internal architecture supports
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 users? It might be a
good idea to do so. I'm willing to make a first attempt at this, though I'm
sure
Do we provide an introduction to Isabelle/jEdit for PG users? It might be a
good idea to do so. I'm willing to make a first attempt at this, though I'm
sure it will contain some mistakes, which I'm sure others of you would be only
too happy to fix.
I have in mind a single webpage, with a
Here are some further data. Mac OS X version 10.8.2.
I was puzzled by slight differences between my setup on my workstation and my
laptop, for example, pressing RETURN performs auto complete on one but not the
other. I couldn't find any generic information about how auto complete works on
I'm having a frustrating time with jEdit key bindings. If I try to redefine an
existing binding, it crashes.
Larry
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
man-days were lost solving the problem. Sure, everybody can update their hgrc
file to refer to lxbroy10, but what happens when it needs to be shut down for
some reason?
Larry
On 3 Jan 2013, at 14:33, Makarius makar...@sketis.net wrote:
On Wed, 2 Jan 2013, Lawrence Paulson wrote:
I have
I have been using
hgbroy.informatik.tu-muenchen.de
under the assumption that the name hgbroy could be expected to refer to a
suitable machine.
Can I continue to do that?
Larry
On 1 Jan 2013, at 21:52, Makarius makar...@sketis.net wrote:
Thanks again for picking up the bright
Surely those files belong in the Isabelle app?
Larry
On 14 Dec 2012, at 14:02, Makarius makar...@sketis.net wrote:
So we merely need to figure out where the .elc stuff is going: Is it in the
component and deleted for other platforms? Is it not in the component, but
created by the
I'm not interested in patching anything unless we see a definite bug fix.
Larry
On 14 Dec 2012, at 12:50, Makarius makar...@sketis.net wrote:
On Wed, 12 Dec 2012, Jasmin Christian Blanchette wrote:
Larry seemed to favor 4.2 (according to the principle that new software is
better than old
But for the Mac version we bundle a specific Emacs binary anyway.
Larry
On 14 Dec 2012, at 12:56, Makarius makar...@sketis.net wrote:
On Wed, 12 Dec 2012, Lawrence Paulson wrote:
I compiled 4.2, no problem.
You mean byte-compiled .el - .elc? This causes a lock-in to a particular
Emacs
That might be a good idea.
The point of a bundle is to put together a combinations of things that are
known to work.
Larry
On 14 Dec 2012, at 13:06, Makarius makar...@sketis.net wrote:
If you say that Isabelle.app should exclusively use the bundled
Is there a verbose option where it says what it's going to do first?
Larry
On 13 Dec 2012, at 08:59, Tobias Nipkow nip...@in.tum.de wrote:
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.
I compiled 4.2, no problem.
I didn't notice any differences with 4.1.
Larry
On 12 Dec 2012, at 18:51, Jasmin Christian Blanchette
jasmin.blanche...@gmail.com wrote:
Am 12.12.2012 um 19:29 schrieb Makarius:
Are there actually Isabelle / Proof General 4.2 users around?
I think Larry
201 - 300 of 416 matches
Mail list logo
