*To*: Holger Blasum <hbl at sysgo.com>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Print Heading *before* theory (nice to have)*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 16 Oct 2013 10:01:20 +0200*In-reply-to*: <20131016074026.GA10199@hbl-lap-dell>*References*: <20131016074026.GA10199@hbl-lap-dell>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

Hi Holger, you can use the header command before the theory starts: header {* Fibonacci *} theory Fib imports Main begin Best, Andreas On 16/10/13 09:40, Holger Blasum wrote:

Dear users, if I encapsulate the fib function (from the tutorial) into a file and want to give it a nice heading ("Fibonacci") I recall I can use the "section" command. $cat fib.thy theory fib imports Main begin section {* Fibonacci *} fun fib :: "nat => nat" where "fib 0 = 0" | "fib (Suc 0) = 1" | "fib (Suc(Suc x)) = fib x + fib (Suc x) end Then a generated PDF looks like this theory fib imports Main begin Fibonacci fun fib :: nat => nat where fib 0 = 0 | fib (Suc 0 ) = 1 | fib (Suc(Suc x )) = fib x + fib (Suc x ) end Is there a simple and maintainable way to move the content of the heading ("Fibonacci") *before* "theory fib"? thx,

**Follow-Ups**:**Re: [isabelle] Print Heading *before* theory (nice to have)***From:*Holger Blasum

**References**:**[isabelle] Print Heading *before* theory (nice to have)***From:*Holger Blasum

- Previous by Date: [isabelle] Print Heading *before* theory (nice to have)
- Next by Date: Re: [isabelle] Print Heading *before* theory (nice to have)
- Previous by Thread: [isabelle] Print Heading *before* theory (nice to have)
- Next by Thread: Re: [isabelle] Print Heading *before* theory (nice to have)
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list