Am 18/04/2012 04:23, schrieb Christian Sternagel:
> +1 for <--> (since it would agree, as Tobias pointed out, with the established
> =>, ==>, ->, -->).
Thanks for actually referring to the topic at hand. The discussion has gotten
completely off topic and became quite fundamentalist. I was merely s
On 04/18/2012 03:56 PM, Christian Sternagel wrote:
On 04/18/2012 03:42 PM, Lawrence Paulson wrote:
How do you do “show me", “commands", “find theorem", “settings", etc?
I believe you're supposed to remember commands for all of those items
and type them explicitly. That's not what a user interfac
On 04/18/2012 03:42 PM, Lawrence Paulson wrote:
How do you do “show me", “commands", “find theorem", “settings", etc? I believe
you're supposed to remember commands for all of those items and type them explicitly. That's not
what a user interface is supposed to do.
Actually I did never use thes
+1 for <--> (since it would agree, as Tobias pointed out, with the
established =>, ==>, ->, -->).
Concerning convenience of input and automatic replacement:
I would not use automatic replacement at all, since it is at least as
often a problem as it is of help (e.g., ML code inside theories "=>
Just for the record: I exclusively use jEdit for several weeks now and
did quite a lot of actual proofs. My personal opinion: the user
experience is much nicer than with emacs
* I did not have any complete hangs yet (as with emacs)
* the whole appearance is much nicer (remember, this is my pers
On Tue, 17 Apr 2012, Alexander Krauss wrote:
On 04/17/2012 05:41 PM, Tobias Nipkow wrote:
This is what I would call unwieldy: instead of typing<--> or<-> (and
having them converted to the appropriate symbols) you always type<->,
but then you have to select from a menue. I don't see the progres
On 04/17/2012 05:41 PM, Tobias Nipkow wrote:
This is what I would call unwieldy: instead of typing<--> or<-> (and having
them converted to the appropriate symbols) you always type<->, but then you
have to select from a menue. I don't see the progress.
Could not agree more. These arrows are ve
Am 17/04/2012 17:56, schrieb Makarius:
> Why then the proposal to change the prover syntax?
What I meant was not just the prover syntax but also the input syntax. In fact,
primarily the input syntax. One could change merely the latter (which is what PG
does), but that introduces an inconsistency:
> Anyway, who is maintaining Isabelle ProofGeneral now? The repository
> version does not work with Emacs 23 for several months already. It seems
> that nobody cares about it anymore.
>
> For the release, I will package up official ProofGeneral-4.1 as last time.
> It is then up to its users t
> Anyway, who is maintaining Isabelle ProofGeneral now? The repository
> version does not work with Emacs 23 for several months already. It seems
> that nobody cares about it anymore.
>
> For the release, I will package up official ProofGeneral-4.1 as last time.
> It is then up to its users
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
On Tue, 17 Apr 2012, Tobias Nipkow wrote:
Am 17/04/2012 16:27, schrieb Lawrence Paulson:
I think you are right that ASCII syntax is almost completely irrelevant now.
Hardly anybody sees it.
It is relevant as an input method, and that is exactly what my
suggestion is about. I am not interest
Am 17/04/2012 16:27, schrieb Lawrence Paulson:
> I think you are right that ASCII syntax is almost completely irrelevant now.
> Hardly anybody sees it.
It is relevant as an input method, and that is exactly what my suggestion is
about. I am not interested in ASCII art but in a smooth input method
Am 17/04/2012 16:13, schrieb Makarius:
> On Tue, 17 Apr 2012, Tobias Nipkow wrote:
>> and would also leave room for an ASCII syntax for \ (namely
>> <->).
>
> Using <--> for <-> and making room for another <-> would also mean that the
> user
> has to type/read the longer unwieldy sequence by def
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
On Tue, 17 Apr 2012, Tobias Nipkow wrote:
In HOL, the ASCII syntax for \ is defined to be <->
but visually <--> would be more appropriate, closer to -->
A brief look at the history and source archive shows that this ASCII art
has already been there since Isabelle86. Larry might still remember
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
In HOL, the ASCII syntax for \ is defined to be <-> but
visually <--> would be more appropriate, closer to --> and would also leave room
for an ASCII syntax for \ (namely <->).
Any views on such a change?
Tobias
___
isabelle-dev mailing list
isabelle-..
On Mon, 26 Oct 2009, Timothy Bourke wrote:
>>> I get the following results for Isabelle 2009 and a recent (yesterday)
>>> dev version:
>>> \version
>>> test \ 2009 dev
>>>+-++
>>>ML | s1 fails | s1 fails |
>>>| s2 wo
On Oct 23 at 16:32 +0200, Makarius wrote:
> On Fri, 23 Oct 2009, Timothy Bourke wrote:
>
>> I'm having some trouble working with ML files in recent dev versions.
>>
>> Given, for example, a file test.ML:
>> structure Test =
>> struct
>>val s1 = "\";
>>val s2 = "\\";
>> end;
>>
>> And
On Fri, 23 Oct 2009, Timothy Bourke wrote:
> I'm having some trouble working with ML files in recent dev versions.
>
> Given, for example, a file test.ML:
> structure Test =
> struct
>val s1 = "\";
>val s2 = "\\";
> end;
>
> And two tests:
> ML) Direct ML: isabelle-process < test.ML
>
I'm having some trouble working with ML files in recent dev versions.
Given, for example, a file test.ML:
structure Test =
struct
val s1 = "\";
val s2 = "\\";
end;
And two tests:
ML) Direct ML: isabelle-process < test.ML
USE) Interactive isabelle: use "test.ML";
I get the follow
22 matches
Mail list logo
