# HG changeset patch
# User paulson
# Date 1059057700 -7200
# Node ID fd6d20c2371c3dd03a7eb02e7d0289a3f8469aa9
# Parent  40a4768c8e0b5a262f715d2b7a2b2c12f0acaffd
header comment

diff -r 40a4768c8e0b -r fd6d20c2371c src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Thu Jul 24 16:37:04 2003 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy	Thu Jul 24 16:41:40 2003 +0200
@@ -1,4 +1,10 @@
-(*Loading further simprocs*)
+(*  Title:      HOL/NatSimprocs.thy
+    ID:         $Id$
+    Copyright   2003 TU Muenchen
+*)
+
+header {*Simprocs for the Naturals*}
+
 theory NatSimprocs = NatBin
 files "int_factor_simprocs.ML" "nat_simprocs.ML":