equal
deleted
inserted
replaced
5 satisfies plus_ac0: + is an AC-operator with zero |
5 satisfies plus_ac0: + is an AC-operator with zero |
6 *) |
6 *) |
7 |
7 |
8 theory HyperOrd = HyperDef: |
8 theory HyperOrd = HyperDef: |
9 |
9 |
10 ML |
|
11 {* |
|
12 val left_distrib = thm"left_distrib"; |
|
13 *} |
|
14 |
10 |
15 (*** Monotonicity results ***) |
11 (*** Monotonicity results ***) |
16 |
12 |
17 lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j; k\<le>l |] ==> i + k < j + l" |
13 lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j; k\<le>l |] ==> i + k < j + l" |
18 by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 add_strict_mono) |
14 by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 add_strict_mono) |