| changeset 57442 | 2373b4c61111 |
| parent 44890 | 22f665a2e91c |
| child 62042 | 6c6ccf573479 |
--- a/src/HOL/Hoare/Arith2.thy Mon Jun 30 10:10:32 2014 +0200 +++ b/src/HOL/Hoare/Arith2.thy Mon Jun 30 10:34:28 2014 +0200 @@ -9,7 +9,7 @@ imports Main begin -definition "cd" :: "[nat, nat, nat] => bool" +definition cd :: "[nat, nat, nat] => bool" where "cd x m n \<longleftrightarrow> x dvd m & x dvd n" definition gcd :: "[nat, nat] => nat"