From bb2f58f761b01dc7346ec6aeb1acb776b8a63cb5 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Mon, 14 Jan 2002 16:58:08 +0000
Subject: tuned;

---
 etc/isar/trace_simp.thy | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'etc')

diff --git a/etc/isar/trace_simp.thy b/etc/isar/trace_simp.thy
index 5a675346..430d37f5 100644
--- a/etc/isar/trace_simp.thy
+++ b/etc/isar/trace_simp.thy
@@ -1,8 +1,9 @@
 
 theory trace_simp = Main:
 
-(* this produces massive amount of simplifier trace, but terminates
-   eventually: *)
+text {*
+  this produces massive amount of simplifier trace, but terminates
+  eventually: *}
 
 ML {* set trace_simp *}
 ML {* reset quick_and_dirty *}
@@ -10,7 +11,7 @@ ML {* reset quick_and_dirty *}
 datatype ord = Zero | Succ ord | Limit "nat => ord"
 
 
-(* this one loops forever *)
+text {* this one loops forever *}
 
 lemma "ALL x. f x = g(f(g(x))) ==> f [] = f [] @ []"
   apply simp
-- 
cgit v1.2.3