some test cases for trace_simp output;

1 files changed, 17 insertions, 0 deletions

diff --git a/etc/isar/trace_simp.thy b/etc/isar/trace_simp.thy
new file mode 100644
index 00000000..5a675346
--- /dev/null
+++ b/etc/isar/trace_simp.thy
@@ -0,0 +1,17 @@
+
+theory trace_simp = Main:
+
+(* this produces massive amount of simplifier trace, but terminates
+   eventually: *)
+
+ML {* set trace_simp *}
+ML {* reset quick_and_dirty *}
+
+datatype ord = Zero | Succ ord | Limit "nat => ord"
+
+
+(* this one loops forever *)
+
+lemma "ALL x. f x = g(f(g(x))) ==> f [] = f [] @ []"
+  apply simp
+