no setup is necessary anymore
authorblanchet
Mon Jun 28 18:47:07 2010 +0200 (2010-06-28)
changeset 37622b3f572839570
parent 37621 3e78dbf7a382
child 37623 295f3a9b44b6
no setup is necessary anymore
src/HOL/Metis_Examples/Tarski.thy
src/HOL/Sledgehammer.thy
     1.1 --- a/src/HOL/Metis_Examples/Tarski.thy	Mon Jun 28 18:46:42 2010 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Tarski.thy	Mon Jun 28 18:47:07 2010 +0200
     1.3 @@ -507,9 +507,8 @@
     1.4  
     1.5  (*never proved, 2007-01-22*)
     1.6  declare [[ atp_problem_prefix = "Tarski__CLF_lubH_is_fixp" ]]
     1.7 -(*Single-step version fails. The conjecture clauses refer to local abstraction
     1.8 -functions (Frees), which prevents expand_defs_tac from removing those 
     1.9 -"definitions" at the end of the proof. *)
    1.10 +(* Single-step version fails. The conjecture clauses refer to local abstraction
    1.11 +functions (Frees). *)
    1.12  lemma (in CLF) lubH_is_fixp:
    1.13       "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
    1.14  apply (simp add: fix_def)
     2.1 --- a/src/HOL/Sledgehammer.thy	Mon Jun 28 18:46:42 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Mon Jun 28 18:47:07 2010 +0200
     2.3 @@ -86,8 +86,6 @@
     2.4  done
     2.5  
     2.6  use "Tools/Sledgehammer/clausifier.ML"
     2.7 -setup Clausifier.setup
     2.8 -
     2.9  use "Tools/Sledgehammer/meson_tactic.ML"
    2.10  setup Meson_Tactic.setup
    2.11