src/HOL/Metis_Examples/Clausification.thy
changeset 50696 85f944352d55
parent 47308 9caab698dbe4
child 50705 0e943b33d907
     1.1 --- a/src/HOL/Metis_Examples/Clausification.thy	Thu Jan 03 13:11:04 2013 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Clausification.thy	Thu Jan 03 13:28:37 2013 +0100
     1.3 @@ -10,10 +10,6 @@
     1.4  imports Complex_Main
     1.5  begin
     1.6  
     1.7 -(* FIXME: shouldn't need this *)
     1.8 -declare [[unify_search_bound = 100]]
     1.9 -declare [[unify_trace_bound = 100]]
    1.10 -
    1.11  
    1.12  text {* Definitional CNF for facts *}
    1.13  
    1.14 @@ -139,7 +135,7 @@
    1.15  lemma
    1.16    "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
    1.17     (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
    1.18 -by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
    1.19 +by (metis split_list_last_prop[where P = P] in_set_conv_decomp)
    1.20  
    1.21  lemma ex_tl: "EX ys. tl ys = xs"
    1.22  using tl.simps(2) by fast