# HG changeset patch
# User wenzelm
# Date 1181053566 -7200
# Node ID b1f3f53c60b5e819ed5d897f9105b82c977f07e2
# Parent  67268bb40b219debaba96d63156df4a16f760718
tuned comments;

diff -r 67268bb40b21 -r b1f3f53c60b5 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Tue Jun 05 16:26:04 2007 +0200
+++ b/src/HOL/Presburger.thy	Tue Jun 05 16:26:06 2007 +0200
@@ -1,9 +1,6 @@
 (*  Title:      HOL/Presburger.thy
     ID:         $Id$
     Author:     Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen
-
-File containing necessary theorems for the proof
-generation for Cooper Algorithm  
 *)
 
 header {* Presburger Arithmetic: Cooper's Algorithm *}
diff -r 67268bb40b21 -r b1f3f53c60b5 src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Jun 05 16:26:04 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Jun 05 16:26:06 2007 +0200
@@ -2,10 +2,8 @@
     ID:         $Id$
     Author:     Amine Chaieb and Tobias Nipkow, TU Muenchen
 
-File containing the implementation of Cooper Algorithm
-decision procedure (intensively inspired from J.Harrison)
-*)
-
+The Cooper Algorithm decision procedure (intensively inspired by
+J. Harrison). *)
 
 signature COOPER_DEC = 
 sig
diff -r 67268bb40b21 -r b1f3f53c60b5 src/HOL/ex/Abstract_NAT.thy
--- a/src/HOL/ex/Abstract_NAT.thy	Tue Jun 05 16:26:04 2007 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy	Tue Jun 05 16:26:06 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Makarius
 *)
 
-header {* Abstract Natural Numbers with polymorphic recursion *}
+header {* Abstract Natural Numbers primitive recursion *}
 
 theory Abstract_NAT
 imports Main