--- 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 *}
--- 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
--- 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