src/HOL/Integ/cooper_dec.ML
changeset 14877 28084696907f
parent 14758 af3b71a46a1c
child 14920 a7525235e20f
equal deleted inserted replaced
14876:477c414000f8 14877:28084696907f
    37   val conjuncts : term -> term list
    37   val conjuncts : term -> term list
    38   val disjuncts : term -> term list
    38   val disjuncts : term -> term list
    39   val has_bound : term -> bool
    39   val has_bound : term -> bool
    40   val minusinf : term -> term -> term
    40   val minusinf : term -> term -> term
    41   val plusinf : term -> term -> term
    41   val plusinf : term -> term -> term
       
    42   val onatoms : (term -> term) -> term -> term
       
    43   val evalc : term -> term
    42 end;
    44 end;
    43 
    45 
    44 structure  CooperDec : COOPER_DEC =
    46 structure  CooperDec : COOPER_DEC =
    45 struct
    47 struct
    46 
    48