diff options
| author | Makarius Wenzel | 2002-01-14 16:58:08 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2002-01-14 16:58:08 +0000 |
| commit | bb2f58f761b01dc7346ec6aeb1acb776b8a63cb5 (patch) | |
| tree | 8c5c198df5dea332b344b052c56fbcb492722707 /etc/isar/trace_simp.thy | |
| parent | e75758c4f574017be99ed5a83d44e4f5c6cc1640 (diff) | |
tuned;
Diffstat (limited to 'etc/isar/trace_simp.thy')
| -rw-r--r-- | etc/isar/trace_simp.thy | 7 |
1 files changed, 4 insertions, 3 deletions
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 |