# HG changeset patch
# User mengj
# Date 1133158538 -3600
# Node ID bbca1d2da0e9b71356b53b97f957822b511ff999
# Parent  e15a825da2629976829cb63963c2907845c149e8
Added two functions for CNF translation, used by other files.

diff -r e15a825da262 -r bbca1d2da0e9 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Mon Nov 28 07:15:13 2005 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Mon Nov 28 07:15:38 2005 +0100
@@ -27,7 +27,8 @@
   val pairname : thm -> (string * thm)
   val repeat_RS : thm -> thm -> thm
   val cnf_axiom_aux : thm -> thm list
-
+  val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list
+  val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list
   end;
 
 structure ResAxioms : RES_AXIOMS =
@@ -394,6 +395,17 @@
 (*works for both FOL and HOL*)
 val cnf_rules = cnf_rules_g cnf_axiom;
 
+fun cnf_rules1 [] err_list = ([],err_list)
+  | cnf_rules1 ((name,th) :: ths) err_list =
+    let val (ts,es) = cnf_rules1 ths err_list
+    in
+	((name,cnf_axiom (name,th)) :: ts,es) handle _ => (ts,(name::es)) end;
+
+fun cnf_rules2 [] err_list = ([],err_list)
+  | cnf_rules2 ((name,th) :: ths) err_list =
+    let val (ts,es) = cnf_rules2 ths err_list
+    in
+	((name,map prop_of (cnf_axiom (name,th))) :: ts,es) handle _ => (ts,(name::es)) end;
 
 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)