Anonymous user
Documentation: Difference between revisions
no edit summary
(→{{header|Wren}}: Changed method name for consistency with 'Fmt' module.) |
No edit summary |
||
Line 773:
* [http://www.cs.arizona.edu/icon/library/src/progs/ipldoc.icn ipldoc.icn] Program to collect library documentation.<br/>
* [http://www.cs.arizona.edu/icon/library/src/progs/iplindex.icn iplindex.icn] Program to produce indexed listing of the program library.
=={{header|Isabelle}}==
<lang Isabelle>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</lang>
| |||