aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/isar/trace_simp.thy
diff options
context:
space:
mode:
Diffstat (limited to 'etc/isar/trace_simp.thy')
-rw-r--r--etc/isar/trace_simp.thy4
1 files changed, 2 insertions, 2 deletions
diff --git a/etc/isar/trace_simp.thy b/etc/isar/trace_simp.thy
index 44f6e5af..de651e5b 100644
--- a/etc/isar/trace_simp.thy
+++ b/etc/isar/trace_simp.thy
@@ -6,8 +6,8 @@ text {*
this produces massive amount of simplifier trace, but terminates
eventually: *}
-declare [[trace_simp]]
-ML {* reset quick_and_dirty *}
+declare [[simp_trace]]
+ML {* quick_and_dirty := false *}
datatype ord = Zero | Succ ord | Limit "nat => ord"