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 wrote:
> On Fri, 2013-03-22 at 13:25 +0100, Makarius wrote:
>> On Fri, 22 Mar 2013, Andreas Lochbihler wrote:
>>
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
https://mailmanbroy
, Lawrence Paulson 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
>
>
> On 18 Mar 2013, at 11:4
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
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 wrote:
>
> On 08/03/13 23:46, Joachim Breitner wrote:
>> Sometimes, when I’m writing apply-script style proofs, I have w
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 wrote:
> This looks just like making the meaning of indentation a bit more formal.
> Lets say as a mode of checking in
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 wrote:
> I actually had that
ore
> difficult. How do you mean? True, it would be hard to compare 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?
>
&
I do think that a simple 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 wrote:
> On Wed, 27 Feb 2013, Lawrence Paulson wrote:
>
>
de needs to be fixed.
Larry
On 27 Feb 2013, at 12:23, Makarius 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) bu
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 wrote:
> Dear a
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 t
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
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 wrote:
> My main problem with the current d
obias
>
> 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)
>>
>> _
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
https://mailmanbroy.informatik.tu-muenchen.de/mailman/list
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 d
h the sledgehammer
execution.
Larry
On 14 Feb 2013, at 17:34, Peter Lammich 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
ferently from just saying, "how did 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 wrote:
> On Thu, 14 Feb 2013, Lawrence Paulson 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 0
One option is simply for me to update my existing PG-based preview to use
Isabelle/jEdit.
At the same time, Christian could perhaps make a webpage by extracting the most
important points from his paper.
Does this idea makes sense?
Larry
On 25 Jan 2013, at 10:16, Makarius wrote:
> On Fri, 25
k 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 Isabell
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 couple
inding
CMD-[, and when it asks whether to overwrite an existing binding, click YES.
Larry
hs_err_pid2302.log
Description: Binary data
On 17 Jan 2013, at 12:59, Makarius wrote:
> On Thu, 17 Jan 2013, Lawrence Paulson wrote:
>
> Depending what you mean by "crash", this hyper
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
jEdit
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
that worked; thanks!
Larry
On 7 Jan 2013, at 15:51, Ondřej Kunčar wrote:
> On 01/07/2013 04:47 PM, Lawrence Paulson wrote:
>> It seems to me that something is fundamentally broken. Every attempt to
>> build anything results in the fo
It seems to me that something is fundamentally broken. Every attempt to build
anything results in the following message.
~/isabelle/Repos/src/HOL: isabelle build
Error: Could not find or load main class isabelle.Build
37091451ba1a tip
Larry
___
isab
re several
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 wrote:
> On Wed, 2 Jan 2013, Lawrence Paulson wrote:
>
>
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 wrote:
> Thanks again for picking up the bright weapons of empirical scie
A very impressive analysis. Thanks.
Larry
On 25 Dec 2012, at 10:38, Alexander Krauss wrote:
> I would say that this points to the SUSE NFS client driver as the source of
> the problem. If we use lxbroy10 exclusively for pushes, we should be safe
> until the issue is fixed.
___
Agree.
Larry
On 21 Dec 2012, at 12:43, Jasmin Christian Blanchette
wrote:
> Skipping a version can be a good solution in the long run. If the bug is in
> Mercurial, then chances are that other people will start reporting similar
> bugs to the Mercurial mailing list, that the maintainers will
Surely those files belong in the Isabelle app?
Larry
On 14 Dec 2012, at 14:02, Makarius 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 administrative script that
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 wrote:
> If you say that Isabelle.app should exclusively use the bundled
> "$THIS/Aquamacs.app/Contents/MacOS/Aquamacs" it should be
But for the Mac version we bundle a specific Emacs binary anyway.
Larry
On 14 Dec 2012, at 12:56, Makarius 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
I'm not interested in patching anything unless we see a definite bug fix.
Larry
On 14 Dec 2012, at 12:50, Makarius 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 software), wher
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 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".
> Renaming
> "buil
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
wrote:
> Am 12.12.2012 um 19:29 schrieb Makarius:
>
>> Are there actually Isabelle / Proof General 4.2 users around?
>
> I think Larry gave it a try.
>
>> For
might
be very confusing.
Larry
On 8 Dec 2012, at 13:18, Makarius 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
>
Surely the existence of two theories of the same name can be detected?
JEdit has been working fine for me for the past couple of weeks (despite
updating regularly and getting new versions). Missing components maybe?
Larry
On 3 Dec 2012, at 21:55, Jasmin Christian Blanchette
wrote:
> Am 03.12
tures.
Larry
On 30 Nov 2012, at 15:27, Makarius 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 docu
It actually makes sense to put every effort into making the jEdit version as
good as possible, especially for beginners. It might be worth investigating
what issues cause them the most problems; I imagine that some sort of short
tutorial video or slideshow (analogous to the one I made a number o
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 wrote:
> * A version of Proof General as Isabelle component, like
>http://isabelle.in.tum.de/components/ProofGeneral-4.1.tar.gz
>(it
I am using version 4.1. I was having problems compiling 4.2, and it doesn't
seem to run in interpreted mode. I'm not sure what is changed between 4.1 and
4.2 anyway.
For the Emacs client, definitely Aquamacs. The other Emacs port is terrible, in
particular because it doesn't behave at all 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 wrote:
> I've had the same experience before, while exchanging theories that
> heavily relied on sledgehammer with other people across different
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 the
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 wrote:
> With the "case that must fail" we are getting back to the tendencies of this
> thread:
> https://mailmanbroy.informatik.tu-muenchen.de/piperm
Good idea. Please ensure that some of them are brand-new users.
Larry
On 5 Sep 2012, at 14:46, Makarius 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 get some impress
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 wrote:
> On 05.09.2012 15:13, Lawrence Paulson wrote:
>> Fixing a variab
absolutely unmissable.
Larry
On 5 Sep 2012, at 14:00, Lars Noschinski 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 >=
Simply fixing too many or too few variables.
Larry
On 5 Sep 2012, at 13:52, Lars Noschinski 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 general type?
>
>
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 wrote:
> Also, this change giv
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 wrote:
> I use -D/document_dump extensively for producing papers. The Isabelle Latex
> output pretty much always requires post processing
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, T
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 int
Agree. I often looked at these. Though they can be confusing in the presence of
multi-threading.
Larry
On 23 Aug 2012, at 14:20, Gerwin Klein wrote:
> I'd be quite keen to get the old behaviour back.
___
isabelle-dev mailing list
isabelle-...@in.tum.d
That would be great - thanks!
Larry
On 22 Aug 2012, at 20:18, Makarius wrote:
> On Tue, 21 Aug 2012, Lawrence Paulson wrote:
>
>> Many thanks for your very detailed response! I wonder what to do next in
>> terms of documenting this method, and perhaps, developing it furth
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 s
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 mo
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
General/path.sc
can tell, the time that a processor spends
> waiting for memory counts as its CPU time unlike when it is waiting for IO.
>
> David
>
> On 08/08/2012 09:00, Lawrence Paulson wrote:
>> I understand about the parallelism, but what has cut back on the memory
>> consumptio
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 :-)
Simply awesome.
Larry
On 7 Aug 2012, at 21:59, Makarius wrote:
> 0:45:45 elapsed time, 8:44:02 cpu time, factor 11.45
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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 requi
sting your changesets? Is there some command to
generate a Mac application?
Larry
On 25 Jul 2012, at 10:36, Makarius wrote:
> On Mon, 23 Jul 2012, Lawrence Paulson wrote:
>
>> What does Platypus actually give us?
>
> See its website, via the URL from my Admi
What does Platypus actually give us?
Once we know how the application should be laid out inside, we don't need
Platypus any more. The application can be the same every time, just with a
fresh copy of Isabelle.
Larry
On 23 Jul 2012, at 19:36, Makarius wrote:
> The Info.plist edited here was ge
ould be able to know 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 the
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 i
I would say that this discussion is better confined to the developers' list.
Entries need to be maintained. This surely includes extending them and
streamlining existing proofs. It surely does not include replacing a
development by entirely different development with related objectives. I don't
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 (w
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 for
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?
http://itunes.apple.
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: type
I may as well be a bit more explicit. About seven Cambridge MPhil students were
given an assignment that included converting the following ML code into HOL and
proving theorems about it.
fun nnf (Atom a) = Atom a
| nnf (Neg (Atom a)) = Neg (Atom a)
| nnf (Neg (Neg p)) = nnf p
| nnf (Neg (C
Thank you for investigating. I have been waiting for Alex to present his view.
Naturally, the current treatment resembles ML's.
I continue to believe that reference to IDEs is a distraction. I've seen
several instances now (in student work) of nonsensical function definitions
caused by putting
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 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 t
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 cli
You seem to be saying that the main difficulty with providing menus is that
they would insert material into the proof script. My own feeling is, if this is
the only way we can have menus, then so be it: without them, we still have to
type in the very same material.
A quirk of the current setup
I am teaching an Isabelle course right now, and I constantly refer students to
various capabilities offered in Proof General's menus. I've never understood
how jEdit can do the amazing things it does and yet not offer something as
simple as menus. To an RSI sufferer, typing commands over and ove
Precisely.
Larry
On 13 May 2012, at 09:44, Florian Haftmann wrote:
> c) I strongly object to clutter the HOL syntax even more than now by
> incorporating just another fancy syntax. I would prefer the lattice
> solution (delete syntax immediately after use and provide a library
> theory to option
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 \ ?a' \ ?f(\<^sup>f ?a := ?b)(\<^sup>f ?a' := ?b') = ?f(\<^su
I disagree. People frequently e-mail problems to one another. Of course, the
ability to paste readable Unicode symbols would be even better, but that's
surely too much to ask right now.
Larry
On 11 May 2012, at 06:33, Christian Sternagel wrote:
> Currently only, copy-pasting examples from jedit
Agree. I think it is a fundamental data structure.
Larry
On 10 May 2012, at 18:46, Lukas Bulwahn wrote:
> Therefore, I am also in strong favour for moving the AFP entry FinFun into
> the distribution.
___
isabelle-dev mailing list
isabelle-...@in.tum.
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 wr
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 t
4/18/2012 03:42 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 mista
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 typ
n Tue, 17 Apr 2012, 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
> a
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 2
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 characters
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 \ is de
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 wrote:
>> * Auxiliary contexts indicate block structure for specifications with
>> additional parameters
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 instantiations
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 an
It looks like I was running 5.3.0, but I found the latest version inside the
bundle. So that's one problem solved.
Larry
On 19 Mar 2012, at 08:38, Jasmin Christian Blanchette wrote:
> Hi Larry,
>
> Am 18.03.2012 um 11:34 schrieb Lawrence Paulson:
>
>> Ano
erating system are you running?
>
> Hope this helps.
> Andrew
>
> On 18/03/2012, at 9:34 PM, Lawrence Paulson wrote:
>
>> I'm doing a demo this week, and find that some symbols don't display
>> properly on my laptop. I've installed the STIX f
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?
>
>
301 - 400 of 538 matches
Mail list logo
