[isabelle-dev] html output of theories

Makarius makarius at sketis.net
Wed Apr 16 14:52:07 CEST 2014

On Mon, 14 Apr 2014, Gottfried Barrow wrote:

> On 14-04-14 05:01, Makarius wrote:
>>  I've recently started to think about adding a bit of Markdown
>>  (https://daringfireball.net/projects/markdown) to the 'text' syntax in a
>>  conservative way, such that there is no LaTeX required for basic things
>>  like itemize/enumerate/description, and it also looks better in the
>>  editor.
> You mentioned markdown a while back, and now I understand it. Like any 
> word, the meaning of "markdown" is going to fragment over time. Now that 
> certain markdowns are standardized, used officially by sites like 
> Stackoverflow, is markdown the workaround that it used to be? I say no, 
> but that's only a side comment.

There are indeed many different versions of "Markdown", each with its own 

The idea was merely to re-use a few of its basic principles, e.g. the way 
paragraphs and itemizations (with nested paragraphs) are recognized. The 
Isabelle document language already has sectioning, and other things like 
hyperlinks, index entries etc. are done by antiquotations.


More information about the isabelle-dev mailing list