equal
deleted
inserted
replaced
10 |
10 |
11 real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)" |
11 real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)" |
12 (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*) |
12 (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*) |
13 real_mult_minus1: "-1 * z = - (z::real)" |
13 real_mult_minus1: "-1 * z = - (z::real)" |
14 real_mult_2: "2 * z = z + (z::real)" |
14 real_mult_2: "2 * z = z + (z::real)" |
|
15 real_diff_0: "0 - x = - (x::real)" |
|
16 |
15 |
17 |
16 ML {* |
18 ML {* |
17 (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var: |
19 (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var: |
18 Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *) |
20 Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *) |
19 |
21 |