From e75758c4f574017be99ed5a83d44e4f5c6cc1640 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Mon, 14 Jan 2002 16:52:51 +0000
Subject: some test cases for trace_simp output;

---
 etc/isar/trace_simp.thy | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 etc/isar/trace_simp.thy

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
+
-- 
cgit v1.2.3