src/HOL/TPTP/TPTP_Parser_Example.thy
changeset 55049 327eafb594ba
parent 53393 5278312037f8
child 63167 0909deb8059b
     1.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Sun Jan 19 11:05:38 2014 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Sun Jan 19 22:38:17 2014 +0100
     1.3 @@ -65,9 +65,9 @@
     1.4  @{assert} (is_some (try (auto_prove @{context}) an_fmlas) = false)
     1.5  *}
     1.6  
     1.7 -sledgehammer_params [provers = remote_z3, debug]
     1.8 +sledgehammer_params [provers = z3, debug]
     1.9  ML {*
    1.10  @{assert} (is_some (try (sh_prove @{context}) an_fmlas) = true)
    1.11  *}
    1.12  
    1.13 -end
    1.14 \ No newline at end of file
    1.15 +end