diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2010-08-20 11:21:59 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2010-08-20 11:21:59 +0000 |
| commit | e03cc0ba6b2a93341f7c59a7cbf6a61ef6a21788 (patch) | |
| tree | 418ea0be9925fc44f9264a7531257699f0c9d740 /etc/isar | |
| parent | 2f18e9ef17cdaef576c1400616375f22adc1d6b1 (diff) | |
declare trace_simp in Isar, not 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 1f56cb35..44f6e5af 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 {* Config.put trace_simp true *} +declare [[trace_simp]] ML {* reset quick_and_dirty *} datatype ord = Zero | Succ ord | Limit "nat => ord" |