src/FOL/simpdata.ML
changeset 11748 06eb315831ff
parent 11344 57b7ad51971c
child 11771 b7b100a2de1d
     1.1 --- a/src/FOL/simpdata.ML	Sun Oct 14 19:59:15 2001 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Sun Oct 14 19:59:55 2001 +0200
     1.3 @@ -369,7 +369,8 @@
     1.4  (* rulify setup *)
     1.5  
     1.6  local
     1.7 -  val ss = FOL_basic_ss addsimps (Drule.norm_hhf_eq :: map Thm.symmetric (thms "atomize"));
     1.8 +  val ss = FOL_basic_ss addsimps
     1.9 +    [Drule.norm_hhf_eq, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
    1.10  in
    1.11  
    1.12  structure Rulify = RulifyFun