2006-08-29 haftmann [Tue, 29 Aug 2006 14:31:13 +0200] rev 20426
added typecopy_package
src/HOL/Tools/datatype_codegen.ML src/HOL/Tools/typecopy_package.ML src/HOL/Typedef.thy

2006-08-29 haftmann [Tue, 29 Aug 2006 14:31:12 +0200] rev 20425
added typecopy_package and some examples
src/HOL/IsaMakefile

2006-08-29 haftmann [Tue, 29 Aug 2006 14:31:11 +0200] rev 20424
updated keywords
etc/isar-keywords-HOL-Nominal.el etc/isar-keywords-ZF.el etc/isar-keywords.el

2006-08-28 paulson [Mon, 28 Aug 2006 18:18:31 +0200] rev 20423
minor bug fixes
src/HOL/Tools/ATP/reduce_axiomsN.ML src/HOL/Tools/res_atp.ML

2006-08-28 paulson [Mon, 28 Aug 2006 18:16:08 +0200] rev 20422
removed the (apparently pointless) signature constraint
src/HOL/Tools/res_clause.ML

2006-08-28 paulson [Mon, 28 Aug 2006 18:15:32 +0200] rev 20421
tidied
src/HOL/Tools/res_axioms.ML src/HOL/Tools/res_hol_clause.ML

2006-08-28 webertj [Mon, 28 Aug 2006 16:10:44 +0200] rev 20420
encode clauses as Isar premises, rather than as object-logic &, for faster parsing
lib/scripts/dimacs2hol.pl

2006-08-25 paulson [Fri, 25 Aug 2006 18:48:58 +0200] rev 20419
abstraction of lambda-expressions
src/HOL/Tools/res_atp.ML src/HOL/Tools/res_axioms.ML

2006-08-25 paulson [Fri, 25 Aug 2006 18:48:09 +0200] rev 20418
tidied
src/HOL/Tools/res_clause.ML

2006-08-25 paulson [Fri, 25 Aug 2006 18:47:36 +0200] rev 20417
better skolemization, using first-order resolution rather than hoping for the right result
src/HOL/Tools/meson.ML