27 lines
581 B
Text
27 lines
581 B
Text
|
theory Text
|
|||
|
|
imports Main
|
|||
|
|
begin
|
|||
|
|
|
|||
|
|
chapter ‹Presenting Theories›
|
|||
|
|
|
|||
|
|
text ‹This text will appear in the proof document.›
|
|||
|
|
|
|||
|
|
section ‹Some Examples.›
|
|||
|
|
|
|||
|
|
― ‹A marginal comment. The expression \<^term>‹True› holds.›
|
|||
|
|
|
|||
|
|
lemma True_is_True: "True" ..
|
|||
|
|
|
|||
|
|
text ‹
|
|||
|
|
The overall content of an Isabelle/Isar theory may alternate between formal
|
|||
|
|
and informal text.
|
|||
|
|
›
|
|||
|
|
|
|||
|
|
text_raw ‹Can also contain raw latex.›
|
|||
|
|
|
|||
|
|
text ‹This text will only compile if the fact @{thm True_is_True} holds.›
|
|||
|
|
|
|||
|
|
text ‹This text will only compile if the constant \<^const>‹True› is defined.›
|
|||
|
|
|
|||
|
|
end
|