diff options
Diffstat (limited to 'etc')
| -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 |