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
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'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
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 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)
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:
*
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
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
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
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
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
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' =
, 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
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:
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
HOL is not building, see attached. Don't ask for the change set
identifier because I couldn't tell you even to save my life. I can
tell you that it has been like this for the past several hours.
Larry
*** Unknown attribute: smt_cert (line 22 of /Users/lp15/isabelle/
I have just done a fetch and can no longer build Isabelle/HOL. I hope
somebody can fix this soon.
Larry
Building HOL ...
HOL FAILED
(see also /Users/lp15/.isabelle/heaps//polyml-5.2.1_x86-darwin/log/HOL)
*** Warning: Pattern is not exhaustive. Found near
*** val ( [ isom_def], cdef_thy) = |(
If you do these things, you put an end to all Isabelle logics other
than Isabelle/HOL. Remember, an object logic does not need to possess
an equality symbol or even an implication symbol.
Having just translated some lengthy, incomprehensible HOL proofs into
Isabelle, I appreciate more than
This sort of discussion is analogous to suggesting that we get rid of
and/or/not/implies and write all formulas using the Scheffer stroke
(NAND), or that Gentzen's sequent calculus should be replaced by the
much simpler Hilbert system. It can be done, but who would want to do
it?
Larry
Anybody know why find theorems can find nothing about the power set operator?
Other set theoretic primitives, such as Union and insert, work fine.
Larry
-- next part --
A non-text attachment was scrubbed...
Name: screen-capture.png
Type: image/png
Size: 24748 bytes
Desc:
Yes, Main is included; see below.
Larry
On 14 Dec 2009, at 12:46, Tobias Nipkow wrote:
I get to see 21 thms. Are you sure Set is included as an ancestor, eg
via Main?
-- next part --
A non-text attachment was scrubbed...
Name: screen-capture-1.png
Type: image/png
Size:
We advertise wwwfind as the leading new feature of Isabelle 2009-1. But how is
it actually invoked?
I could find no mention of it in PG. On my Mac, it does this:
~: isabelle wwwfind
Platform Darwin currently not supported by wwwfind component.
On a Linux workstation, it does this:
rhee:
for each and every machine that needs to have
lighttpd installed. This is quite a deterrent :-(
Larry
On 19 Jan 2010, at 22:11, Gerwin Klein wrote:
On 19/01/2010, at 9:33 PM, Lawrence Paulson wrote:
We advertise wwwfind as the leading new feature of Isabelle 2009-1. But how
is it actually
Ideally one could select between the standard libraries, the full libraries
(everything within HOL) and the AFP by a menu. But there is no need to
overcomplicate it the first time. The default should just be HOL/Library.
Larry
On 20 Jan 2010, at 11:13, Gerwin Klein wrote:
This would be a good
I'm not sure what has gone wrong with my system. I don't think I have changed
anything. It may be that I downloaded and recompiled poly/ML. Now I can't build
Isabelle any more:
Loading theory Complex_Main
val it = () : unit
Error occurred during initialization of VM
Unable to load native
Thank you for doing this. It's interesting that you have found a shorter
formalisation, because the approach previously adopted had been carefully
selected to require the minimum effort.
I agree that the old formalisation should be kept somewhere (possibly in the
AFP) because comparing
I have looked at this ancient code again, and think I understand the problem.
prove_conv is mostly used to prove the conclusion of the simproc. If the two
terms are equal, then it is unwanted, so the correct response is to fail. That
is why the aconv test is there.
But occasionally,
it again, but that was
after hours of work. Perhaps something is different about our systems. I'm
using a Mac with snow leopard.
Larry
On 17 May 2010, at 10:46, Makarius wrote:
On Sat, 15 May 2010, Lawrence Paulson wrote:
I've used PG Version 4.0pre091204 quite a bit, no problems. What goes wrong
Equalities involving constants have never been eliminated in this way. The
equality must involve a variable, free or bound. The method has no way of
knowing about constraints on the variable that are not part of the goal. In the
case of a structured proof, it would be appropriate and natural to
.
Yours,
Thomas.
___
From: isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de
[isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de] On Behalf Of
Lawrence Paulson [l...@cam.ac.uk]
Sent: Tuesday, June 15, 2010 1:12 AM
To: Brian Huffman
Cc: isabelle
If there is an easy way to identify free variables that are constrained
externally, then such a change would be beneficial. Failing that, the
particular case of locales is particularly necessary to handle correctly.
Larry
On 15 Jun 2010, at 14:17, Brian Huffman wrote:
Note that testing
. This is
bad advice if “auto” can render the problem impossible to prove.
Larry
On 15 Jun 2010, at 10:17, Jasmin Christian Blanchette wrote:
Am 15.06.2010 um 11:03 schrieb Lawrence Paulson:
Altering the behaviour of the safe method on locale constants might be
feasible, because it would
This practically goes back to the dawn of time. Any theorem produced by
resolution would be beta-eta-normal. And this includes most theorems, but
certainly not all.
Larry
On 4 Aug 2010, at 02:50, Thomas Sewell wrote:
Hello Isabelle developers.
I was about to have another attempt at
This sort of thing is well-known but very rare these days. I guess it could
trap an unwary user. It just isn't easy to fix, given the old strategy of using
assumptions, discarding them, and repeating.
Larry
On 5 Aug 2010, at 06:33, John Matthews wrote:
Was it ever resolved whether auto should
Thanks for looking into this problem, which has been around in one way or
another from the very beginning.
Lost in all the technical discussions is the question of what the user will
see. We have the option of leaving blast and force as they are now to minimise
danger of incompatibility,
This sounds logical. But what about auto? Like the other three, it is used to
perform obvious steps in a proof, and it is not terminal.
Larry
On 1 Sep 2010, at 14:17, Thomas Sewell wrote:
Let me try to explain the difference from the perspective of a user. There
are three classical tools
I always intended auto to be initial rather than terminal. I'm not aware of the
unsafe mode you refer to, but it may have been introduced later.
Larry
On 1 Sep 2010, at 14:40, Thomas Sewell wrote:
Good point - I think of auto as terminal. My understanding was that auto had
both a safe and
That is certainly my change, but I don't understand why preventing
self-referential type instantiations should affect the find_theorems function.
Can you get a full trace back from the exception?
Larry
On 18 Nov 2010, at 16:03, Brian Huffman wrote:
Hello everyone,
Recently I noticed that
, Michael Chan wrote:
On 18/11/10 16:07, Lawrence Paulson wrote:
I can't see the answer to this, but something complicated is going on when
you match (?f::((?'a=?'b)=?'c)) ?stuff against x y where x :: nat = nat.
Thanks, Larry. Indeed, even without the predicate, it gives the same problem
Indeed I find the code peculiar, in that it delivers the higher-order matchers
followed by the first-order ones. But these are different things. And I imagine
there is often redundancy.
Larry
On 19 Nov 2010, at 15:50, Michael Chan wrote:
On 19/11/10 14:10, Lawrence Paulson wrote:
If you look
I agree!
Larry
On 2 Dec 2010, at 14:44, Brian Huffman wrote:
Besides these two very specific cases, I think it would be best to
reject definitions with extra type variables on the right-hand side.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
I'm afraid that English wine production has been increasing year by year. Some
of them are even said to be good.
http://www.english-wine.com/vineyards.html
Larry
On 7 Jan 2011, at 09:30, Tobias Nipkow wrote:
I like the wine connection! Not just French wines, but also Australian
ones, and
Obviously this proposal would involve a significant incompatibility. It may not
even be very relevant any more, as this sort of instantiation is rather out of
fashion. But it is worth a discussion.
Larry
Begin forwarded message:
I would propose to simplify the parsing rules to work like this:
2011, at 17:19, Brian Huffman wrote:
On Tue, Feb 8, 2011 at 9:01 AM, Lawrence Paulson l...@cam.ac.uk wrote:
Historically, the point is that index numbers were regarded as very
important in variable names, while identifiers ending with digits were not
seen as important. And there are other ways
This indeed is probably one of the chief reasons for the existing arrangements.
Larry
On 9 Feb 2011, at 08:36, Alexander Krauss wrote:
An incompatibility that will not be reported by tests is that
intermediate goal states, where nonzero indexnames are quite frequent,
will look significantly
Does anybody know what to do here?
Larry
~/isabelle/Repos: hg push
pushing to http://isabelle.in.tum.de/repos/isabelle
searching for changes
http authorization required
realm: Mercurial repositories
user:
___
isabelle-dev mailing list
It looks like this exception is raised when gconv_rule cv i th is called and
the specified subgoal does not exist. The function gconv_rule is called in only
four places in Pure:
./Isar/element.ML: (Conv.gconv_rule Drule.beta_eta_conversion 1 r)
./raw_simplifier.ML: then Conv.gconv_rule
Thank you for looking there! This is the most plausible culprit. But it is
strange that this problem has arisen before.
A possible fix is to replace the last line of the function timing_depth_tac in
that file as follows:
handle PROVE = Seq.empty | THM _ = Seq.empty;
Andreas, do you want to
Awesome! It looks positively industrial in scale.
Larry
On 30 May 2011, at 08:54, Alexander Krauss wrote:
Hi all,
In the past weeks, there has been some progress with our new testing
infrastructure, which I would like to summarize here. Please give
feedback, ask questions, and discuss.
My impression from fooling around a little is that this is a bug that has been
around for a year and a half. The comment seems to suggest that | no longer
works as an index item (even when protected using), so we have to give up
index entries for the symbols | and |-|. I wonder whether there is
It seems it can be fixed by
(a) using ! rather than | as the sort key (the sorting of special symbols is
arbitrary anyway)
(b) using \char124 to denote the | symbol
I would expect to see this problem in any index entry involving the | symbol.
Larry
On 30 May 2011, at 14:58, Lawrence Paulson
There were broken index entries in most of the old documentation. For some
reason, the | symbol didn't cause a problem in the tutorial. One index entry
here was fixed to use ?? (as opposed to !) as the sort key.
Larry
On 30 May 2011, at 15:28, Lawrence Paulson wrote:
It seems it can be fixed
Is it possible to restrict command completion to a select collection of
commonly used commands? Or to make it the user-configurable?
Larry
On 24 Jun 2011, at 21:01, Alexander Krauss wrote:
Suggestion: Simply kill completion of commands (not symbols)???
Is there any real cost to having so many type classes?
Larry
On 8 Jul 2011, at 02:13, Brian Huffman wrote:
The drawback to this design is that it requires yet another type
class, of which we have plenty already.
___
isabelle-dev mailing list
We appear to be in danger of overlooking this problem, which could indicate a
significant error somewhere. The names of bound variables should not be
significant. Does anybody have any idea what could be causing this?
Larry
Begin forwarded message:
From: Lars Noschinski nosch...@in.tum.de
It's clear that for inductive definitions, relations are frequently more
natural than sets. But I wonder whether a less drastic solution could have been
found than abandoning sets altogether. (I'm trying to imagine some sort of
magic operator to ease the transition between sets with various
I am currently working on AFP/Coinductive, which is full of the sort of thing.
Larry
On 19 Aug 2011, at 00:31, Gerwin Klein wrote:
Can't really quantify it, but I'm seeing this all the time from not-so-novice
users over here. Mixing sets and predicates (e.g. using intersection on
To avoid duplication of effort, note that I'm currently trying to convert the
AFP theories DataRefinementIBP and GraphMarkingIBP.
Larry
___
isabelle-dev mailing list
isabelle-...@in.tum.de
I've come across something strange in the file
isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if
anybody could think of an explanation.
A proof works only if I insert before it the following:
instance set :: (type) complete_boolean_algebra
proof
qed (auto simp add:
I'm starting to have doubts about this entire procedure.
I thought the plan was to get these theories (particularly in the AFP) into a
state where they no longer dependent on confusing sets with predicates so that
they would work with either version of Isabelle. I'm not sure that's possible.
I
I've just been trying to get the proofs working, not to simplify them or even
to understand them. Incidentally, let there be no illusions about people
accidentally stumbling into a mixture of sets and predicates. Some of these
theories were clearly designed from the ground upwards on the
indeed yes I'm the person who decided that this primitive should introduce a
type as a copy of an existing non-empty set. I have always preferred sets to
predicates and the examples I have looked at lately have only strengthened my
view. Not to mention numerous occasions when people have
I shall take a look at this one. If anybody else is working on it, please let
me know as soon as possible.
Larry
On 25 Aug 2011, at 21:45, Florian Haftmann wrote:
HOL-Probability FAILED
___
isabelle-dev mailing list
isabelle-...@in.tum.de
I am trying to process the following declaration in Probability/Sigma_Algebra:
inductive_set
smallest_ccdi_sets :: ('a, 'b) algebra_scheme \Rightarrow 'a set set
.
.
.
monos Pow_mono
I get the following error message (for the version with set types):
*** Bad monotonicity theorem:
***
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 list
I think this is a good idea.
Larry
On 22 Sep 2011, at 03:08, Brian Huffman wrote:
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
Legacy.thy that would not be imported by default, and would be
cleared out
A suggestion and some compliments...
Larry
Begin forwarded message:
From: James Frank s...@gmx.com
Subject: Needed ghostscript package to build PDF in Cygwin
Date: 5 October 2011 15:54:30 GMT+01:00
To: l...@cam.ac.uk
Dear Dr. Paulson,
The problem I had with building the Isabelle PDF
If my memory is correct, quicksort was the clear winner in the performance
tests that I undertook for my book.
Larry
On 27 Oct 2011, at 13:50, Florian Haftmann wrote:
interesting to read that comment. The exiting quicksort implementation
in HOL is indeed taken from Isabelle's ML library.
I did quite a few of these conversions. Generally the changes were
straightforward, EXCEPT for theories that explicitly treated sets as
predicates. In the former case, the strategy is to rigorously confine yourself
to set primitives, but in the latter case, you may find yourself with a
I remember when you could build a logic by typing “isabelle make, and if an
error occurred somewhere, it would terminate with an error message.
I am trying to make textual changes now, and I find that “isabelle make simply
hangs. if I terminate it, I discover where I have introduced some sort
I think I've worked this out. Something was looping in a parallel thread
probably.
Larry
On 6 Mar 2012, at 12:00, Lawrence Paulson wrote:
I remember when you could build a logic by typing “isabelle make, and if an
error occurred somewhere, it would terminate with an error message.
I am
I have tried both,And they are better at different things. I still find
MacMercurial more intuitive for the basics.
Larry
On 7 Mar 2012, at 14:34, Makarius wrote:
On Wed, 7 Mar 2012, Lawrence Paulson wrote:
There is also MacMercurial, which gives access to all the basic commands
That's
Also in ZF/Inductive_ZF.thy...
Larry
On 16 Mar 2012, at 10:35, Lawrence Paulson wrote:
I have a problem with the current version (9ff441f295c2). See attachment.
This prevents the use of PG within ZF. However, it builds at the command
line. What is supposed to be here?
Screen Shot 2012-03
I have redirected your request to isabelle-us...@cl.cam.ac.uk. That is the
appropriate mailing list for users' questions.
The developers' mailing list is for use by the Isabelle developers.
Larry Paulson
On 27 Mar 2012, at 09:14, charmi panchal wrote:
Hello,
I am a beginner of Isabelle and
There is something I'd like to mention, not a big deal, but worth considering.
I've been doing some proofs lately after a long gap, making myself a
combination of a novice and expert. And I've got confused by things that would
probably confuse true novices even more.
Here are two
I look forward to seeing some documentation on these increasingly mysterious
constructs… :-)
Larry
On 16 Apr 2012, at 11:14, Brian Huffman wrote:
On Sun, Apr 15, 2012 at 2:54 PM, Makarius makar...@sketis.net wrote:
* Auxiliary contexts indicate block structure for specifications with
I don't really mind, and I imagine that there aren't many uses at the moment,
so you could get away with it.
On the other hand, it does create an incompatibility between HOL and FOL (and
therefore ZF).
Larry
On 17 Apr 2012, at 07:35, Tobias Nipkow wrote:
In HOL, the ASCII syntax for
As regards motivation, remember, back then it was a thing of beauty. I could
easily remember the day when it was possible to use lowercase letters.
I think you are right that ASCII syntax is almost completely irrelevant now.
Hardly anybody sees it. Even on my MacBook where the Unicode
I certainly care about it. Jedit is great for browsing existing theory
developments, but there is no support for actually doing proofs.
Larry
On 17 Apr 2012, at 16:56, Makarius wrote:
Anyway, who is maintaining Isabelle ProofGeneral now? The repository version
does not work with Emacs 23
, Lawrence Paulson wrote:
I certainly care about it. Jedit is great for browsing existing theory
developments, but there is no support for actually doing proofs.
As I've said already 4 years ago, the double burden to keep ProofGeneral
alive and make Isabelle/jEdit a full replacement (and more
This sounds like a good idea. The old notation was pretty unreadable.
Larry
On 19 Apr 2012, at 12:11, Tobias Nipkow wrote:
Currently, the sort of a type variable in a type is constrained by attaching
::S to it. Right in the middel of the type, eg 'a::ord = 'a = bool. This
can make types less
PM, Lawrence Paulson wrote:
A further problem is you cannot cut and paste between the “proof window
and the main window, so good luck creating any structured proofs (unless
you love typing lots of formal text and never make mistakes). And on a Mac,
the keyboard shortcuts are different from
That is a good one! The one I need is C-C C-A C-Q ...
Larry
On 20 Apr 2012, at 18:00, Makarius wrote:
On Fri, 20 Apr 2012, Lawrence Paulson wrote:
Cut and paste works much better with this version!
I still have to get to grips with a lot of very basic things
For me it has required 2
It works for me, and the auto-detect is nice.
The option to download for arbitrary platforms is occasionally useful, but
isn't worth making a big effort. A simple link or button labelled “other
platforms or “show all platforms should be sufficient.
Larry
On 26 Apr 2012, at 13:09, Makarius
I'm glad we are going to move the theory into the repository. However, I would like to discuss the issue of its syntax. The presence of the letter “f" in the apply and update notation is fatal to readability:lemma finfun_update_twist: ?a \noteq ?a' \Longrightarrow ?f(\^supf ?a := ?b)(\^supf ?a' :=
This does work now, maybe my problem was with the repository version.
Larry
On 16 May 2012, at 15:01, Makarius wrote:
I don't see what you mean. In Isabelle2012-RC2 I can type sl, wait 300ms,
press RETURN, and see sledgehammer running and producing Output
incrementally. Then I can click
I am marking some student work submitted for the Cambridge Isabelle course, and
have seen some examples where students have gone terribly wrong because they
overlooked the warning “Ignoring redundant equation in a function definition.
This sort of mistake could happen to anybody, and it means
I'm not talking about user interfaces or models. I am saying that function
definitions containing entirely redundant equations should be rejected, also in
batch mode.
Larry
On 29 May 2012, at 15:32, Makarius wrote:
The warnings were shown nicely in the Prover IDE, although some fine points
I've probably overlooked something. Where is the current version kept?
Larry
### Building Isabelle/jEdit ...
src/scala_console.scala:21: error: IMain is not a member of
scala.tools.nsc.interpreter
import scala.tools.nsc.interpreter.IMain
^
src/scala_console.scala:43: error: not found:
MacHg is pretty good, and now that I've learnt never to use FileMerge for
merging (because it crashes, meaning you lose your work every time there's a
conflict), I finally find Mercurial tolerable.
However, I'm curious about a rival client, SourceTree. Has anybody tried it?
This is obviously a bug.
Does anybody know (without going to the trouble of reproducing this exact proof
and obtaining a backtrace) why the function dest_equals is being called on a
sort constraint? At a guess, something is expecting a definition.
Larry
Begin forwarded message:
Oh, I
Thanks for investigating. Although he made a mistake, of course, we should
deliver an intelligible error message and not simply allow an exception to
propagate.
Larry
On 6 Jul 2012, at 13:56, Makarius wrote:
On Tue, 3 Jul 2012, Lawrence Paulson wrote:
Does anybody know (without going
Recent Isabelle applications for Mac don't seem to recognise the .thy filename
extension, and Mac OS is unwilling to assign them as the default application
for theory files. I believe that the fix is as follows:
(1), to use the attached version of Info.plist and
(2), to include the attached
how to deal with that.
Larry
On 23 Jul 2012, at 17:41, Makarius wrote:
On Mon, 23 Jul 2012, Lawrence Paulson wrote:
Recent Isabelle applications for Mac don't seem to recognise the .thy
filename extension, and Mac OS is unwilling to assign them as the default
application for theory files. I
On 25 Jul 2012, at 15:22, Makarius wrote:
On Wed, 25 Jul 2012, Lawrence Paulson wrote:
What would be involved in testing your changesets? Is there some command to
generate a Mac application?
Yes, it is the Admin/MacOS/App1/mk script.
The requirements are explained in Admin/MacOS/App1
I understand about the parallelism, but what has cut back on the memory
consumption?
Larry
On 7 Aug 2012, at 21:59, Makarius wrote:
Most processes stay in the 1GB range, the formerly bulky JinjaThreads
stabilizes at comformtable 2.5-3.5 GB.
We have to find new ways to waste memory :-)
What am I doing wrong? isabelle build HOL is the same.
Larry
~/isabelle/Repos/src/HOL: isabelle build
### Building Isabelle/Scala layer ...
Changed files:
Concurrent/simple_thread.scala
General/exn.scala
General/file.scala
General/graph.scala
General/linear_set.scala
That is indeed good news. Would it be appropriate to advise users to upgrade,
is there are no immediate need?
Larry
On 16 Aug 2012, at 16:39, Makarius wrote:
Oracle has released the important Java 7u6 yesterday, see also
http://www.oracle.com/us/corporate/press/1735645
It means much more
As far as I am aware, we provide no documentation on the “algebra proof method.
My impression is that this method will prove anything that it can convert to
the form
p1 = 0 == … == pn = 0 == p = 0
where p1, …, pn, p are polynomials, possibly in multiple variables, over a
suitable
1 - 100 of 416 matches
Mail list logo
