changeset 16417 | 9bc16273c2d4 |
parent 15647 | b1f486a9c56b |
child 17188 | a26a4fc323ed |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
1 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *) |
1 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *) |
2 |
2 |
3 theory HOL4Real = HOL4Base: |
3 theory HOL4Real imports HOL4Base begin |
4 |
4 |
5 ;setup_theory realax |
5 ;setup_theory realax |
6 |
6 |
7 lemma HREAL_RDISTRIB: "ALL x y z. |
7 lemma HREAL_RDISTRIB: "ALL x y z. |
8 hreal_mul (hreal_add x y) z = hreal_add (hreal_mul x z) (hreal_mul y z)" |
8 hreal_mul (hreal_add x y) z = hreal_add (hreal_mul x z) (hreal_mul y z)" |