I recently had a number of problems with Mercurial. The cause of one
of them turned out to be that Mercurial doesn't interact with MacOS X
very well, so although the commit command launches an editor to
request a commit message, this message never reaches mercurial.
But a more serious
Possibly of interest to Mac users. It is particularly good at
monitoring the status of your local files and comparing them with your
local repository.
http://www.jwwalker.com/pages/macmerc.html
Larry
-- next part --
An HTML attachment was scrubbed...
URL:
, at 19:02, David Aspinall wrote:
Lawrence Paulson wrote:
Does anybody know what would cause the symbols that look like this?
It is the latest version of proof general running under GNU Emacs
22.2.1
Nobody else came running so I'll answer...
First of all: everyone will have a *much* better
The offending code is here:
fun fol_terms_to_hol ctxt fol_tms =
let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
val _ = Output.debug (fn () = calling type inference:)
val _ = app (fn t = Output.debug (fn () =
Syntax.string_of_term ctxt t)) ts
val ts' =
We implement a nice syntax for summations indexed over intervals, but
nothing comparable products. The code below is from the file
SetInterval.thy. Products are treated instead in the file
Finite_Set.thy. Is there a fundamental reason why sums and products
are treated so differently?
Larry
Mac users may want to try this user interface to mercurial. It makes
it easy to do the most common tasks, including fetch, push, commit and
also to display differences. It is less good at showing differences
between your copy of a file and the remote copy.
MacMercurial is a graphic user
When I introduced these constants, they were certainly necessary.
Then, binary arithmetic executed by pure rewriting. I don't object to
getting rid of them if they are now unnecessary. But it hardly seems
worth investing a significant effort. They don't cause a problem, do
they? It may be
What is the difference between willundefined and arbitrary?
Larry
On 2 Oct 2008, at 18:44, Tobias Nipkow wrote:
undefined and default are used in a specific way. If you do not
want
that functionality (and accidental equalities), arbitrary is a good
alternative.
Tobias
Florian Haftmann
Apologies for that garbled message. I meant,
What is the difference between undefined and arbitrary?
Larry
On 2 Oct 2008, at 18:44, Tobias Nipkow wrote:
undefined and default are used in a specific way. If you do not
want
that functionality (and accidental equalities), arbitrary
The error that he refers to concerns the relative links in the
following HTML source code:
ul lia href=HOL/index.htmlHOL (Higher-Order Logic)/a is a
version of classical higher-order logic resembling that of the a
href=http://www.cl.cam.ac.uk/Research/HVG/HOL/;HOL System/a./li
lia
Unfortunately I don't know the answer to this. I have copied this
message to the developers mailing list and maybe somebody else can
help you.
Larry
On 21 Aug 2008, at 11:02, Norbert Voelker wrote:
Larry/Tobias,
the Isabelle2008 News contain the following intriguing sentence:
*
I am happy with this. I just wanted to remind everybody that the
nonstandard system allows really simple, intuitive proofs.
Larry
On 2 Jul 2008, at 17:45, Brian Huffman wrote:
Here's how I see it: If all you want to do is *use* analysis (e.g.
maybe you just want to calculate derivatives)
I see a giant misconception coming. The point of nonstandard analysis
is that it makes properties of limits, derivatives, and so forth much
easier to prove than can be done with the standard definitions. They
eliminate the necessity of arguments involving epsilon and delta. So
it would be
I'm sure you are right. We could try taking it out, though I suspect
this will break many proofs.
Larry
On 10 Oct 2007, at 12:03, Tobias Nipkow wrote:
I have had problems with the conversion from ~ x = (0::nat) to x
0 as
well. Can anyone recall why we installed that? I suspect it may
It needs at least Hilbert_Choice. It could go before Datatype. Some
details need to be worked out to ensure that all theorems in Main.thy
get converted to clause form.
Larry
On 14 Sep 2007, at 14:46, Florian Haftmann wrote:
A PreList-Sledgehammer would be a nice thing to have, but it is not
I have just committed a new version with various changes, including
support for structured proofs with a new version of Vampire. Please
download a new Vampire binary from http://www.cl.cam.ac.uk/research/
hvg/Isabelle/atp-linkup.html (Linux only) if you use Vampire.
The environment variables
401 - 416 of 416 matches
Mail list logo
