Summary
- treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd
The file was modified | src/HOL/Decision_Procs/MIR.thy (diff) |
The file was modified | src/HOL/GCD.thy (diff) |
The file was modified | src/HOL/Decision_Procs/MIR.thy (diff) |
The file was modified | src/HOL/GCD.thy (diff) |