equal
deleted
inserted
replaced
196 val t' = lint vars t |
196 val t' = lint vars t |
197 in |
197 in |
198 if is_numeral s' then (linear_cmul (dest_numeral s') t') |
198 if is_numeral s' then (linear_cmul (dest_numeral s') t') |
199 else if is_numeral t' then (linear_cmul (dest_numeral t') s') |
199 else if is_numeral t' then (linear_cmul (dest_numeral t') s') |
200 |
200 |
201 else (warning "lint: apparent nonlinearity"; raise COOPER) |
201 else raise COOPER |
202 end |
202 end |
203 |_ => error ("COOPER:lint: unknown term \n"); |
203 |_ => raise COOPER; |
204 |
204 |
205 |
205 |
206 |
206 |
207 (* ------------------------------------------------------------------------- *) |
207 (* ------------------------------------------------------------------------- *) |
208 (* Linearize the atoms in a formula, and eliminate non-strict inequalities. *) |
208 (* Linearize the atoms in a formula, and eliminate non-strict inequalities. *) |