src/HOL/ATP.thy
changeset 58142 d6a2e3567f95
parent 57714 4856a7b8b9c3
child 58406 539cc471186f
     1.1 --- a/src/HOL/ATP.thy	Tue Sep 02 14:40:32 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Tue Sep 02 16:38:26 2014 +0200
     1.3 @@ -135,7 +135,7 @@
     1.4  
     1.5  (* Has all needed simplification lemmas for logic.
     1.6     "HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
     1.7 -lemmas waldmeister_fol = simp_thms(1-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
     1.8 +lemmas waldmeister_fol = simp_thms(1,2,4-8,11-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
     1.9    eq_ac disj_comms disj_assoc conj_comms conj_assoc
    1.10  
    1.11