Re: [isabelle] Print Heading *before* theory (nice to have)



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,





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.