26 lines
581 B
Text
26 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
|