105 int_mult ~> of_nat_mult |
105 int_mult ~> of_nat_mult |
106 int_Suc ~> of_nat_Suc |
106 int_Suc ~> of_nat_Suc |
107 inj_int ~> inj_of_nat |
107 inj_int ~> inj_of_nat |
108 int_1 ~> of_nat_1 |
108 int_1 ~> of_nat_1 |
109 int_0 ~> of_nat_0 |
109 int_0 ~> of_nat_0 |
|
110 Lcm_empty_nat ~> Lcm_empty |
|
111 Lcm_empty_int ~> Lcm_empty |
|
112 Lcm_insert_nat ~> Lcm_insert |
|
113 Lcm_insert_int ~> Lcm_insert |
|
114 comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd |
|
115 comp_fun_idem_gcd_int ~> comp_fun_idem_gcd |
|
116 comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm |
|
117 comp_fun_idem_lcm_int ~> comp_fun_idem_lcm |
|
118 Lcm_eq_0 ~> Lcm_eq_0_I |
|
119 Lcm0_iff ~> Lcm_0_iff |
|
120 Lcm_dvd_int ~> Lcm_least |
|
121 divides_mult_nat ~> divides_mult |
|
122 divides_mult_int ~> divides_mult |
|
123 lcm_0_nat ~> lcm_0_right |
|
124 lcm_0_int ~> lcm_0_right |
|
125 lcm_0_left_nat ~> lcm_0_left |
|
126 lcm_0_left_int ~> lcm_0_left |
|
127 dvd_gcd_D1_nat ~> dvd_gcdD1 |
|
128 dvd_gcd_D1_int ~> dvd_gcdD1 |
|
129 dvd_gcd_D2_nat ~> dvd_gcdD2 |
|
130 dvd_gcd_D2_int ~> dvd_gcdD2 |
|
131 coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff |
|
132 coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff |
110 realpow_minus_mult ~> power_minus_mult |
133 realpow_minus_mult ~> power_minus_mult |
111 realpow_Suc_le_self ~> power_Suc_le_self |
134 realpow_Suc_le_self ~> power_Suc_le_self |
|
135 dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest |
112 INCOMPATIBILITY. |
136 INCOMPATIBILITY. |
113 |
137 |
114 |
138 |
115 New in Isabelle2016 (February 2016) |
139 New in Isabelle2016 (February 2016) |
116 ----------------------------------- |
140 ----------------------------------- |