

See also

 Related task: Comments
 Related task: Here_document


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