Documentation: Difference between revisions
Content added Content deleted
(→{{header|Wren}}: Changed method name for consistency with 'Fmt' module.) |
No edit summary |
||
| Line 773: | 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/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. |
* [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> |
|||