might
be very confusing.
Larry
On 8 Dec 2012, at 13:18, Makarius makar...@sketis.net wrote:
On Mon, 3 Dec 2012, Lawrence Paulson wrote:
Surely the existence of two theories of the same name can be detected?
The deeper problem here is that theories still have the ancient flat name
space
.
Larry
On 30 Nov 2012, at 15:27, Makarius makar...@sketis.net wrote:
On Fri, 30 Nov 2012, Lawrence Paulson wrote:
I imagine that some sort of short tutorial video or slideshow (analogous to
the one I made a number of years ago) might be better than any amount of
written documentation.
I've
Will it run without compiled files? And will it run efficiently enough?
Certainly I've always compiled my copy.
Larry
On 21 Nov 2012, at 10:35, Makarius makar...@sketis.net wrote:
* A version of Proof General as Isabelle component, like
The long-term solution must be to deliver self-contained proof scripts, but
obviously it will be difficult.
Larry
On 8 Nov 2012, at 11:51, Tjark Weber webe...@in.tum.de wrote:
I've had the same experience before, while exchanging theories that
heavily relied on sledgehammer with other people
I haven't studied the conditions in detail, but apparently the new licence for
Z3 allows redistribution. And I imagine that allows it to be distributed as
Isabelle component of sledgehammer.
Larry
http://research.microsoft.com/en-us/um/people/leonardo/blog/2012/10/02/open-z3.html
Releasing
Does anybody understand the attached message, which seems to involve the new
build system?
Larry
~/isabelle/Repos/src/HOL: isabelle build HOL-ex
### Missing Isabelle component:
/Users/lp15/.isabelle/contrib/exec_process-1.0.2
Running HOL-ex …
~/isabelle/Repos/src/HOL: hg id
74ad6ecf2af2 tip
If it is unambiguously wrong, then the highlighting must be as bold as in the
case of a syntax error.
Larry
On 5 Sep 2012, at 14:35, Makarius makar...@sketis.net wrote:
With the case that must fail we are getting back to the tendencies of this
thread:
Something of this general sort would certainly be useful. Having the wrong
assumption is the most insidious of errors. The only similar one is misusing
fix. It would be great to be told when your context is wrong.
Larry
On 5 Sep 2012, at 13:45, Lars Noschinski nosch...@in.tum.de wrote:
Also,
Simply fixing too many or too few variables.
Larry
On 5 Sep 2012, at 13:52, Lars Noschinski nosch...@in.tum.de wrote:
Which scenario do you have in mind with fix? The case where a too general
type is chosen, because the first mention of the fixed variable also
type-checks for a more
be absolutely unmissable.
Larry
On 5 Sep 2012, at 14:00, Lars Noschinski nosch...@in.tum.de wrote:
On 05.09.2012 14:54, Lawrence Paulson wrote:
Simply fixing too many or too few variables.
Fixing to many variables should not be a problem, i.e.
lemma !!n :: nat. n = 0
proof -
fix a b
I'm only talking about cases where “show must inevitably fail. Fortunately,
such situations are rare, but if they can easily be detected, they should be.
Larry
On 5 Sep 2012, at 14:20, Lars Noschinski nosch...@in.tum.de wrote:
On 05.09.2012 15:13, Lawrence Paulson wrote:
Fixing a variable
Good idea. Please ensure that some of them are brand-new users.
Larry
On 5 Sep 2012, at 14:46, Makarius makar...@sketis.net wrote:
What I need is to watch over the shoulders of more people trying to write
Isar proofs in the current Prover IDE. In May this year I had 15 people and
2 days to
This has always been my approach as well. Long ago I wrote a little script for
post-processing the latex files.
Larry
On 29 Aug 2012, at 07:16, Gerwin Klein gerwin.kl...@nicta.com.au wrote:
I use -D/document_dump extensively for producing papers. The Isabelle Latex
output pretty much always
Various projects of mine, going back many years, have supported Poly/ML at the
rate of £1000 per year. (That's just under €1300.) This is a much better use of
grant money than to give it to already wealthy publishers for the sake of
so-called Gold open access.
Larry
On 27 Aug 2012, at 16:18,
This sounds like a good plan. And thanks for your further details about how to
integrate an external Gröbner basis tool. Do you think this might be of a
suitable level of difficulty for an MPhil student?
I also noticed the paper that you presented in Birmingham in 2008. Has that
worked been
Many thanks for your very detailed response! I wonder what to do next in terms
of documenting this method, and perhaps, developing it further. Is there a
latex source for the information you sent? It could be added to the
documentation somewhere: but where?
Or would it make sense to integrate
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
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
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
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 :-)
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
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
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
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
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?
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:
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
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'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' :=
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
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
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
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
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
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 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
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 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
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 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
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.
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
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
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
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 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
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 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 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
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
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
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
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)???
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
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
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
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
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:
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
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
, 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
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
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
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 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
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 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
.
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
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
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
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,
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
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
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:
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:
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
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
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) = |(
301 - 400 of 416 matches
Mail list logo
