264 | @{const_name HOL.less_eq} => SOME (p, i, "<=", q, j) |
264 | @{const_name HOL.less_eq} => SOME (p, i, "<=", q, j) |
265 | "op =" => SOME (p, i, "=", q, j) |
265 | "op =" => SOME (p, i, "=", q, j) |
266 | _ => NONE |
266 | _ => NONE |
267 end handle Zero => NONE; |
267 end handle Zero => NONE; |
268 |
268 |
269 fun of_lin_arith_sort sg (U : typ) : bool = |
269 fun of_lin_arith_sort thy U = |
270 Type.of_sort (Sign.tsig_of sg) (U, ["Ring_and_Field.ordered_idom"]) |
270 Sign.of_sort thy (U, ["Ring_and_Field.ordered_idom"]); |
271 |
271 |
272 fun allows_lin_arith sg (discrete : string list) (U as Type (D, [])) : bool * bool = |
272 fun allows_lin_arith sg (discrete : string list) (U as Type (D, [])) : bool * bool = |
273 if of_lin_arith_sort sg U then |
273 if of_lin_arith_sort sg U then |
274 (true, D mem discrete) |
274 (true, D mem discrete) |
275 else (* special cases *) |
275 else (* special cases *) |