equal
deleted
inserted
replaced
6 theory Delete imports "../ProgLang/Language" begin |
6 theory Delete imports "../ProgLang/Language" begin |
7 |
7 |
8 axioms (* theorems which are available only with long names, |
8 axioms (* theorems which are available only with long names, |
9 which can not yet be handled in isac's scripts *) |
9 which can not yet be handled in isac's scripts *) |
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 |
13 real_mult_minus1: "-1 * z = - (z::real)" |
|
14 real_mult_2: "2 * z = z + (z::real)" |
14 |
15 |
15 ML {* |
16 ML {* |
16 (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var: |
17 (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var: |
17 Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *) |
18 Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *) |
18 |
19 |