diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-02-18 00:47:57 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-02-18 00:47:57 +0000 |
| commit | eb77606c2cbbb758627da1aeb73c18f09b2198c2 (patch) | |
| tree | 342d3d9092941feb7ccced34dcaa454809515b56 /isar | |
| parent | 82ec8a535f3c3bb2c9cce4c715ded745085d25d8 (diff) | |
Decoration to show off MMM mode
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/Example.thy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index fc72c2f7..c86bf89a 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -6,7 +6,7 @@ theory Example = Main: -text {* Proper proof text -- naive version. *} +text {* Proper proof text -- \textit{naive version}. *} theorem and_comms: "A & B --> B & A" proof @@ -20,7 +20,7 @@ proof qed -text {* Proper proof text -- advanced version. *} +text {* Proper proof text -- \textit{advanced version}. *} theorem "A & B --> B & A" proof |