changeset 74101 | d804e93ae9ff |
parent 73109 | 783406dd051e |
child 74965 | 9469d9223689 |
--- a/src/HOL/GCD.thy Sun Aug 01 23:18:13 2021 +0200 +++ b/src/HOL/GCD.thy Mon Aug 02 10:01:06 2021 +0000 @@ -31,7 +31,7 @@ section \<open>Greatest common divisor and least common multiple\<close> theory GCD - imports Groups_List + imports Groups_List Code_Numeral begin subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>