src/HOL/Metis_Examples/Clausification.thy
changeset 55417 01fbfb60c33e
parent 50705 0e943b33d907
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Metis_Examples/Clausification.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Clausification.thy	Wed Feb 12 08:37:06 2014 +0100
     1.3 @@ -138,7 +138,7 @@
     1.4  by (metis split_list_last_prop[where P = P] in_set_conv_decomp)
     1.5  
     1.6  lemma ex_tl: "EX ys. tl ys = xs"
     1.7 -using tl.simps(2) by fast
     1.8 +using list.sel(3) by fast
     1.9  
    1.10  lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
    1.11  by (metis ex_tl)