changeset 16417 | 9bc16273c2d4 |
parent 15863 | 78db9506cc78 |
child 24893 | b8ef7afe3a6b |
1.1 --- a/src/ZF/ex/Primes.thy Fri Jun 17 11:35:35 2005 +0200 1.2 +++ b/src/ZF/ex/Primes.thy Fri Jun 17 16:12:49 2005 +0200 1.3 @@ -6,7 +6,7 @@ 1.4 1.5 header{*The Divides Relation and Euclid's algorithm for the GCD*} 1.6 1.7 -theory Primes = Main: 1.8 +theory Primes imports Main begin 1.9 constdefs 1.10 divides :: "[i,i]=>o" (infixl "dvd" 50) 1.11 "m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"