src/FOL/simpdata.ML
changeset 9889 8802b140334c
parent 9851 e22db9397e17
child 10431 bb67f704d631
     1.1 --- a/src/FOL/simpdata.ML	Thu Sep 07 20:48:51 2000 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Sep 07 20:49:19 2000 +0200
     1.3 @@ -1,9 +1,9 @@
     1.4 -(*  Title:      FOL/simpdata
     1.5 +(*  Title:      FOL/simpdata.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1994  University of Cambridge
     1.9  
    1.10 -Simplification data for FOL
    1.11 +Simplification data for FOL.
    1.12  *)
    1.13  
    1.14  
    1.15 @@ -356,3 +356,19 @@
    1.16  open Clasimp;
    1.17  
    1.18  val FOL_css = (FOL_cs, FOL_ss);
    1.19 +
    1.20 +
    1.21 +(* rulify setup *)
    1.22 +
    1.23 +local
    1.24 +  val ss = FOL_basic_ss addsimps (Drule.norm_hhf_eq :: map Thm.symmetric (thms "atomize"));
    1.25 +in
    1.26 +
    1.27 +structure Rulify = RulifyFun
    1.28 + (val make_meta = Simplifier.simplify ss
    1.29 +  val full_make_meta = Simplifier.full_simplify ss);
    1.30 +
    1.31 +structure BasicRulify: BASIC_RULIFY = Rulify;
    1.32 +open BasicRulify;
    1.33 +
    1.34 +end;