--- a/src/HOL/Metis_Examples/Clausify.thy Thu Apr 14 11:24:04 2011 +0200
+++ b/src/HOL/Metis_Examples/Clausify.thy Thu Apr 14 11:24:04 2011 +0200
@@ -8,6 +8,14 @@
imports Complex_Main
begin
+text {* Outstanding issues *}
+
+lemma ex_tl: "EX ys. tl ys = xs"
+using tl.simps(2) by fast
+
+lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
+using [[metis_new_skolemizer = false]] (* FAILS with "= true" *)
+by (metis ex_tl)
text {* Definitional CNF for goal *}
@@ -38,7 +46,6 @@
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
by (metisFT pax)
-
text {* New Skolemizer *}
declare [[metis_new_skolemizer]]