1.1 --- a/src/HOL/Integ/cooper_dec.ML	Sat Jun 05 13:08:53 2004 +0200
     1.2 +++ b/src/HOL/Integ/cooper_dec.ML	Sat Jun 05 18:34:06 2004 +0200
     1.3 @@ -39,6 +39,8 @@
     1.4    val has_bound : term -> bool
     1.5    val minusinf : term -> term -> term
     1.6    val plusinf : term -> term -> term
     1.7 +  val onatoms : (term -> term) -> term -> term
     1.8 +  val evalc : term -> term
     1.9  end;
    1.10  
    1.11  structure  CooperDec : COOPER_DEC =