equal
deleted
inserted
replaced
4 Copyright 1999 TU Muenchen |
4 Copyright 1999 TU Muenchen |
5 |
5 |
6 Augmentation of real linear arithmetic with rational coefficient handling |
6 Augmentation of real linear arithmetic with rational coefficient handling |
7 *) |
7 *) |
8 |
8 |
|
9 val real_divide_1 = thm"real_divide_1"; |
|
10 |
9 local |
11 local |
10 |
12 |
|
13 val times_divide_eq_left = thm"times_divide_eq_left"; |
|
14 val times_divide_eq_right = thm"times_divide_eq_right"; |
|
15 |
11 (* reduce contradictory <= to False *) |
16 (* reduce contradictory <= to False *) |
12 val simps = [True_implies_equals,inst "w" "number_of ?v" real_add_mult_distrib2, |
17 val simps = [True_implies_equals, |
13 real_divide_1,real_times_divide1_eq,real_times_divide2_eq]; |
18 inst "w" "number_of ?v" real_add_mult_distrib2, |
|
19 real_divide_1,times_divide_eq_right,times_divide_eq_left]; |
14 |
20 |
15 val simprocs = [real_cancel_numeral_factors_divide]; |
21 val simprocs = [real_cancel_numeral_factors_divide]; |
16 |
22 |
17 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
23 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
18 |
24 |