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