From eb77606c2cbbb758627da1aeb73c18f09b2198c2 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 18 Feb 2003 00:47:57 +0000
Subject: Decoration to show off MMM mode

---
 isar/Example.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'isar/Example.thy')

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
-- 
cgit v1.2.3