--- 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.
*)
--- 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
--- 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;
+