equal
deleted
inserted
replaced
230 let val T = fastype_of t; |
230 let val T = fastype_of t; |
231 val zero = Const(@{const_name HOL.zero}, T); |
231 val zero = Const(@{const_name HOL.zero}, T); |
232 val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT); |
232 val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT); |
233 val pos = less $ zero $ t and neg = less $ t $ zero |
233 val pos = less $ zero $ t and neg = less $ t $ zero |
234 fun prove p = |
234 fun prove p = |
235 Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p) |
235 Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p) |
236 handle THM _ => NONE |
236 handle THM _ => NONE |
237 in case prove pos of |
237 in case prove pos of |
238 SOME th => SOME(th RS pos_th) |
238 SOME th => SOME(th RS pos_th) |
239 | NONE => (case prove neg of |
239 | NONE => (case prove neg of |
240 SOME th => SOME(th RS neg_th) |
240 SOME th => SOME(th RS neg_th) |