equal
deleted
inserted
replaced
4 |
4 |
5 header {* Semiring normalization *} |
5 header {* Semiring normalization *} |
6 |
6 |
7 theory Semiring_Normalization |
7 theory Semiring_Normalization |
8 imports Numeral_Simprocs Nat_Transfer |
8 imports Numeral_Simprocs Nat_Transfer |
9 uses |
9 begin |
10 "Tools/semiring_normalizer.ML" |
10 |
11 begin |
11 ML_file "Tools/semiring_normalizer.ML" |
12 |
12 |
13 text {* Prelude *} |
13 text {* Prelude *} |
14 |
14 |
15 class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel + |
15 class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel + |
16 assumes crossproduct_eq: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" |
16 assumes crossproduct_eq: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" |