src/FOL/simpdata.ML
changeset 11771 b7b100a2de1d
parent 11748 06eb315831ff
child 12038 343a9888e875
     1.1 --- a/src/FOL/simpdata.ML	Sun Oct 14 22:08:29 2001 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Sun Oct 14 22:15:07 2001 +0200
     1.3 @@ -364,20 +364,3 @@
     1.4  open Clasimp;
     1.5  
     1.6  val FOL_css = (FOL_cs, FOL_ss);
     1.7 -
     1.8 -
     1.9 -(* rulify setup *)
    1.10 -
    1.11 -local
    1.12 -  val ss = FOL_basic_ss addsimps
    1.13 -    [Drule.norm_hhf_eq, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
    1.14 -in
    1.15 -
    1.16 -structure Rulify = RulifyFun
    1.17 - (val make_meta = Simplifier.simplify ss
    1.18 -  val full_make_meta = Simplifier.full_simplify ss);
    1.19 -
    1.20 -structure BasicRulify: BASIC_RULIFY = Rulify;
    1.21 -open BasicRulify;
    1.22 -
    1.23 -end;