diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-19 10:02:53 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-19 10:02:53 +0000 |
| commit | 45a8299de5d20a6ab0d8ffb817d8a6c818067eaa (patch) | |
| tree | 39bf4a91af837921c0e0499b5aabb1e3873e7e5f /etc/isar | |
| parent | abaac3f212e53316d9cb9ac4211066d089b6925c (diff) | |
Update ML (but still doesn't work: how to turn on tracing in ML?)
Diffstat (limited to 'etc/isar')
| -rw-r--r-- | etc/isar/trace_simp.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/etc/isar/trace_simp.thy b/etc/isar/trace_simp.thy index 06458a84..1f56cb35 100644 --- a/etc/isar/trace_simp.thy +++ b/etc/isar/trace_simp.thy @@ -6,7 +6,7 @@ text {* this produces massive amount of simplifier trace, but terminates eventually: *} -ML {* set trace_simp *} +ML {* Config.put trace_simp true *} ML {* reset quick_and_dirty *} datatype ord = Zero | Succ ord | Limit "nat => ord" |