# HG changeset patch
# User blanchet
# Date 1302773044 -7200
# Node ID 4e4f0665e5be5ad76164c79f4215af61fbdce833
# Parent  0e5d1e5e1177949fe76656c8f48f3694367dac47
added outstanding issue to Metis example

diff -r 0e5d1e5e1177 -r 4e4f0665e5be src/HOL/Metis_Examples/Clausify.thy
--- 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]]