changeset 14877 | 28084696907f |
parent 14758 | af3b71a46a1c |
child 14920 | a7525235e20f |
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Sat Jun 05 13:08:53 2004 +0200 +++ b/src/HOL/Tools/Presburger/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 =