Re: [isabelle-dev] Remaining uses of Proof General?
Great list Peter! * The standard search (Ctrl-F) function does not allow to enter non-ASCII characters at all. This is a real show-stopper if you search for a text containing such characters. In PG, you could at least use \... - tokens to enter non-ASCII characters. Moreover, I would like an incremental search, but there is probably a jEdit pluging somewhere? (Probably with the same problems of entering non-ASCII characters) There is already an incremental search, but by default it has no keyboard shortcut. Myself, I have re-bound Ctrl-F to Incremental Search Bar, and am quite happy with that. (This is in jEdit's Global Options, then Shortcuts.) John ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Help
Hi Adamu, You'd be better off asking isabelle-us...@cl.cam.ac.uk for help. Or even Stack Exchange (http://stackoverflow.com/questions/tagged/isabelle). This mailing list is for Isabelle developers, not Isabelle users. Best wishes, john On 11 Jun 2014, at 12:45, Adamu sani yahaya adamusaniyah...@gmail.com wrote: Hello, Please how can I define and declare a tail recursion of factorial with Isabelle/HOL and tail recursive of Reverse with Isabelle/HOL Thanks ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] html output of theories
Hi Makarius,
A general observation is that Isabelle/jEdit has become more and more a live
document browser, now even with Navigator (e.g. in current
Isabelle/282f3b06fa86). So one could also ask the question what is still
missing to eliminate the need for separate HTML browsing.
I think separate HTML browsing is very important, and should not be eliminated.
I can think of three instances where it is very helpful.
[Attracting new Isabelle users.] Alice is browsing the web, stumbles upon
MyIsabelleTheory.html, finds it impressively readable (what with all the
properly-formatted text{*...*} blocks, the hyperlinked structure, the
self-documenting tooltips, the syntax highlighting, etc), and wants to download
Isabelle herself. Even with new features for improved usability and document
browsing, Isabelle/jEdit can't compete with the web-browser for user
familiarity.
[Sharing Isabelle theories with non-Isabellers.] Bob is the guy who knows
Isabelle on the research team, so he formalises the new proof system that the
other researchers come up with. He can't expect the other researchers to
download Isabelle/jEdit, so he sends them a link to the .html pages that they
can read, to see what he's been up to.
[Viewing the result of antiquotations, and so on.] After typing out lots of
antiquotations and so on inside my text{*...*} and header{*...*} blocks, I
would like to see what these will look like in the finished product. I don't
want to print it out, so I have no interest in a boring monochrome paginated
PDF -- I just want my theory to look like it does in Isabelle/jEdit, but with
the antiquotations properly rendered. And I think HTML is probably the right
tool for that.
Best wishes,
John
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] html output of theories
Hi all,
I've been thinking about and playing with the theory to HTML feature of
Isabelle. The PDF output is handy for producing papers, but I do find HTML so
much easier to read onscreen than PDFs. I mostly use Isabelle/jEdit for
browsing theories, but I think HTML output is still very important, e.g. so
that people who don't have Isabelle installed can still read my theories.
Here is a little attempt at a prototype of what Option.thy might look like
after being exported to HTML.
https://dl.dropboxusercontent.com/u/26024007/isabelle/Option.html
For comparison, here is the original:
http://isabelle.in.tum.de/library/HOL/HOL/Option.html
And here is the PDF output (not very readable onscreen, and not interactive):
http://isabelle.in.tum.de/library/HOL/HOL/document.pdf (page 357)
Here is a list of some of the things I've tried to do in this prototype:
1. Interpret text and header commands so that they break out of the
Isabelle source. This is like what happens in the PDF output. The current
browser_info doesn't do this.
2. More syntax highlighting, like in Isabelle/jEdit. I only bothered to do this
for the first couple of lemmas. The current browser_info doesn't have much
syntax highlighting.
3. Hyperlinks, like in Isabelle/jEdit. If you hover your mouse over imports
Datatype, you'll see there's a link to Datatype.html. Same if you hover over
the induct method. Not that these links currently work, of course.
4. Abolishing double-quotes. I don't think they're necessary for presentation,
and they often confuse Isabelle newbies anyway. Instead, I've tried to make
*all* of Isabelle's inner-syntax formatted in a uniform way (namely, shaded in
a slightly darker grey).
5. More symbols rendered properly. The current browser_info doesn't produce a
proper rightharpoonup symbol; my new prototype produces the right unicode
symbol for this.
One problem with all this is that the contents of text {* ... *} is generally
written in LaTeX. It would be desirable if this could also be exported to HTML.
Maybe one has to resort to using something like HeVeA?
By the way, I don't think I have the time or expertise to make much progress on
this beyond this little prototype. I just wanted to start a little discussion
with anybody else who has any thoughts about HTML output of Isabelle theories.
Best wishes,
John
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] html output of theories
Thanks Larry. Sorry, but I don't see any difference in the indentation, at
least not in safari or chrome. Can you point out a line that's wrong?
Sent from my iPhone
On 12 Apr 2014, at 17:01, Lawrence Paulson l...@cam.ac.uk wrote:
Looks nice. Just the indenting needs fixing.
Larry
On 12 Apr 2014, at 11:58, John Wickerson johnwicker...@cantab.net wrote:
Hi all,
I've been thinking about and playing with the theory to HTML feature of
Isabelle. The PDF output is handy for producing papers, but I do find HTML
so much easier to read onscreen than PDFs. I mostly use Isabelle/jEdit for
browsing theories, but I think HTML output is still very important, e.g. so
that people who don't have Isabelle installed can still read my theories.
Here is a little attempt at a prototype of what Option.thy might look like
after being exported to HTML.
https://dl.dropboxusercontent.com/u/26024007/isabelle/Option.html
For comparison, here is the original:
http://isabelle.in.tum.de/library/HOL/HOL/Option.html
And here is the PDF output (not very readable onscreen, and not interactive):
http://isabelle.in.tum.de/library/HOL/HOL/document.pdf (page 357)
Here is a list of some of the things I've tried to do in this prototype:
1. Interpret text and header commands so that they break out of the
Isabelle source. This is like what happens in the PDF output. The current
browser_info doesn't do this.
2. More syntax highlighting, like in Isabelle/jEdit. I only bothered to do
this for the first couple of lemmas. The current browser_info doesn't have
much syntax highlighting.
3. Hyperlinks, like in Isabelle/jEdit. If you hover your mouse over imports
Datatype, you'll see there's a link to Datatype.html. Same if you hover
over the induct method. Not that these links currently work, of course.
4. Abolishing double-quotes. I don't think they're necessary for
presentation, and they often confuse Isabelle newbies anyway. Instead, I've
tried to make *all* of Isabelle's inner-syntax formatted in a uniform way
(namely, shaded in a slightly darker grey).
5. More symbols rendered properly. The current browser_info doesn't produce
a proper rightharpoonup symbol; my new prototype produces the right
unicode symbol for this.
One problem with all this is that the contents of text {* ... *} is
generally written in LaTeX. It would be desirable if this could also be
exported to HTML. Maybe one has to resort to using something like HeVeA?
By the way, I don't think I have the time or expertise to make much progress
on this beyond this little prototype. I just wanted to start a little
discussion with anybody else who has any thoughts about HTML output of
Isabelle theories.
Best wishes,
John
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] html output of theories
Hm, it seems that different browsers interpret the CSS white-space property
in different ways. (Who'd have thought?) It's better now, thanks for pointing
it out.
John
On 12 Apr 2014, at 17:55, Lawrence Paulson l...@cam.ac.uk wrote:
I see no indentation at all, e.g.
enriched_type map: Option.map proof -
fix f g
show Option.map f o Option.map g = Option.map (f o g)
proof
fix x
show (Option.map f o Option.map g) x= Option.map (f o g) x
by (cases x) simp_all
qed
next
show Option.map id = id
proof
fix x
show Option.map id x = id x
by (cases x) simp_all
qed
qed
(in Safari)
Larry
On 12 Apr 2014, at 17:18, John Wickerson johnwicker...@cantab.net wrote:
Thanks Larry. Sorry, but I don't see any difference in the indentation, at
least not in safari or chrome. Can you point out a line that's wrong?
Sent from my iPhone
On 12 Apr 2014, at 17:01, Lawrence Paulson l...@cam.ac.uk wrote:
Looks nice. Just the indenting needs fixing.
Larry
On 12 Apr 2014, at 11:58, John Wickerson johnwicker...@cantab.net wrote:
Hi all,
I've been thinking about and playing with the theory to HTML feature of
Isabelle. The PDF output is handy for producing papers, but I do find HTML
so much easier to read onscreen than PDFs. I mostly use Isabelle/jEdit for
browsing theories, but I think HTML output is still very important, e.g.
so that people who don't have Isabelle installed can still read my
theories.
Here is a little attempt at a prototype of what Option.thy might look
like after being exported to HTML.
https://dl.dropboxusercontent.com/u/26024007/isabelle/Option.html
For comparison, here is the original:
http://isabelle.in.tum.de/library/HOL/HOL/Option.html
And here is the PDF output (not very readable onscreen, and not
interactive):
http://isabelle.in.tum.de/library/HOL/HOL/document.pdf (page 357)
Here is a list of some of the things I've tried to do in this prototype:
1. Interpret text and header commands so that they break out of the
Isabelle source. This is like what happens in the PDF output. The current
browser_info doesn't do this.
2. More syntax highlighting, like in Isabelle/jEdit. I only bothered to do
this for the first couple of lemmas. The current browser_info doesn't have
much syntax highlighting.
3. Hyperlinks, like in Isabelle/jEdit. If you hover your mouse over
imports Datatype, you'll see there's a link to Datatype.html. Same if
you hover over the induct method. Not that these links currently work,
of course.
4. Abolishing double-quotes. I don't think they're necessary for
presentation, and they often confuse Isabelle newbies anyway. Instead,
I've tried to make *all* of Isabelle's inner-syntax formatted in a uniform
way (namely, shaded in a slightly darker grey).
5. More symbols rendered properly. The current browser_info doesn't
produce a proper rightharpoonup symbol; my new prototype produces the
right unicode symbol for this.
One problem with all this is that the contents of text {* ... *} is
generally written in LaTeX. It would be desirable if this could also be
exported to HTML. Maybe one has to resort to using something like HeVeA?
By the way, I don't think I have the time or expertise to make much
progress on this beyond this little prototype. I just wanted to start a
little discussion with anybody else who has any thoughts about HTML output
of Isabelle theories.
Best wishes,
John
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
