src/HOL/ex/Argo_Examples.thy
changeset 69015 5eb493b51bf6
parent 66301 8a6a89d6cf2b
child 74735 0580ae467ecb
equal deleted inserted replaced
69014:a2c042364efc 69015:5eb493b51bf6
   617 end
   617 end
   618 
   618 
   619 
   619 
   620 subsection \<open>Larger examples\<close>
   620 subsection \<open>Larger examples\<close>
   621 
   621 
   622 declare[[argo_trace = basic, argo_timeout = 60]]
   622 declare[[argo_trace = basic, argo_timeout = 120]]
   623 
   623 
   624 
   624 
   625 text \<open>Translated from TPTP problem library: PUZ015-2.006.dimacs\<close>
   625 text \<open>Translated from TPTP problem library: PUZ015-2.006.dimacs\<close>
   626 
   626 
   627 lemma assumes 1: "~x0"
   627 lemma assumes 1: "~x0"