# HG changeset patch
# User wenzelm
# Date 1256828925 -3600
# Node ID 49cd8abb2863c45ca6382300750f0db8729c5deb
# Parent  44f9665c20911144439c3206efca890150ff606e
proper header;

diff -r 44f9665c2091 -r 49cd8abb2863 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Oct 29 16:08:23 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 29 16:08:45 2009 +0100
@@ -1,4 +1,5 @@
-(*  Author: Jia Meng, Cambridge University Computer Laboratory
+(*  Title:      HOL/Tools/res_axioms.ML
+    Author:     Jia Meng, Cambridge University Computer Laboratory
 
 Transformation of axiom rules (elim/intro/etc) into CNF forms.
 *)
diff -r 44f9665c2091 -r 49cd8abb2863 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Thu Oct 29 16:08:23 2009 +0100
+++ b/src/HOL/Tools/res_clause.ML	Thu Oct 29 16:08:45 2009 +0100
@@ -1,11 +1,12 @@
-(*  Author: Jia Meng, Cambridge University Computer Laboratory
-    Copyright 2004 University of Cambridge
+(*  Title:      HOL/Tools/res_clause.ML
+    Author:     Jia Meng, Cambridge University Computer Laboratory
 
-Storing/printing FOL clauses and arity clauses.
-Typed equality is treated differently.
+Storing/printing FOL clauses and arity clauses.  Typed equality is
+treated differently.
+
+FIXME: combine with res_hol_clause!
 *)
 
-(*FIXME: combine with res_hol_clause!*)
 signature RES_CLAUSE =
 sig
   val schematic_var_prefix: string
diff -r 44f9665c2091 -r 49cd8abb2863 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Thu Oct 29 16:08:23 2009 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML	Thu Oct 29 16:08:45 2009 +0100
@@ -1,5 +1,5 @@
-(*
-   Author: Jia Meng, NICTA
+(*  Title:      HOL/Tools/res_hol_clause.ML
+    Author:     Jia Meng, NICTA
 
 FOL clauses translated from HOL formulae.
 *)
@@ -527,4 +527,5 @@
       length helper_clauses + 1, length tfree_clss + length dfg_clss)
   end;
 
-end
+end;
+