diff -r 477c414000f8 -r 28084696907f src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Sat Jun 05 13:08:53 2004 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Sat Jun 05 18:34:06 2004 +0200
@@ -39,6 +39,8 @@
   val has_bound : term -> bool
   val minusinf : term -> term -> term
   val plusinf : term -> term -> term
+  val onatoms : (term -> term) -> term -> term
+  val evalc : term -> term
 end;
 
 structure  CooperDec : COOPER_DEC =