# HG changeset patch
# User wenzelm
# Date 968352559 -7200
# Node ID 8802b140334c0a2eb48306ebcc91197a850c8f6f
# Parent  c5622848bf18e21b9827e9f7ffe4791aa646a57c
rulify setup;

diff -r c5622848bf18 -r 8802b140334c src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Sep 07 20:48:51 2000 +0200
+++ b/src/FOL/simpdata.ML	Thu Sep 07 20:49:19 2000 +0200
@@ -1,9 +1,9 @@
-(*  Title:      FOL/simpdata
+(*  Title:      FOL/simpdata.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Simplification data for FOL
+Simplification data for FOL.
 *)
 
 
@@ -356,3 +356,19 @@
 open Clasimp;
 
 val FOL_css = (FOL_cs, FOL_ss);
+
+
+(* rulify setup *)
+
+local
+  val ss = FOL_basic_ss addsimps (Drule.norm_hhf_eq :: map Thm.symmetric (thms "atomize"));
+in
+
+structure Rulify = RulifyFun
+ (val make_meta = Simplifier.simplify ss
+  val full_make_meta = Simplifier.full_simplify ss);
+
+structure BasicRulify: BASIC_RULIFY = Rulify;
+open BasicRulify;
+
+end;