tuned comments;
authorwenzelm
Tue Jun 05 16:26:06 2007 +0200 (2007-06-05)
changeset 23253b1f3f53c60b5
parent 23252 67268bb40b21
child 23254 99644a53f16d
tuned comments;
src/HOL/Presburger.thy
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/ex/Abstract_NAT.thy
     1.1 --- a/src/HOL/Presburger.thy	Tue Jun 05 16:26:04 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Tue Jun 05 16:26:06 2007 +0200
     1.3 @@ -1,9 +1,6 @@
     1.4  (*  Title:      HOL/Presburger.thy
     1.5      ID:         $Id$
     1.6      Author:     Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen
     1.7 -
     1.8 -File containing necessary theorems for the proof
     1.9 -generation for Cooper Algorithm  
    1.10  *)
    1.11  
    1.12  header {* Presburger Arithmetic: Cooper's Algorithm *}
     2.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Jun 05 16:26:04 2007 +0200
     2.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Jun 05 16:26:06 2007 +0200
     2.3 @@ -2,10 +2,8 @@
     2.4      ID:         $Id$
     2.5      Author:     Amine Chaieb and Tobias Nipkow, TU Muenchen
     2.6  
     2.7 -File containing the implementation of Cooper Algorithm
     2.8 -decision procedure (intensively inspired from J.Harrison)
     2.9 -*)
    2.10 -
    2.11 +The Cooper Algorithm decision procedure (intensively inspired by
    2.12 +J. Harrison). *)
    2.13  
    2.14  signature COOPER_DEC = 
    2.15  sig
     3.1 --- a/src/HOL/ex/Abstract_NAT.thy	Tue Jun 05 16:26:04 2007 +0200
     3.2 +++ b/src/HOL/ex/Abstract_NAT.thy	Tue Jun 05 16:26:06 2007 +0200
     3.3 @@ -3,7 +3,7 @@
     3.4      Author:     Makarius
     3.5  *)
     3.6  
     3.7 -header {* Abstract Natural Numbers with polymorphic recursion *}
     3.8 +header {* Abstract Natural Numbers primitive recursion *}
     3.9  
    3.10  theory Abstract_NAT
    3.11  imports Main