| changeset 5227 | e5a6ace920a0 |
| parent 5148 | 74919e8f221c |
| child 6073 | fba734ba6894 |
--- a/src/HOL/ex/Primes.ML Fri Jul 31 10:54:39 1998 +0200 +++ b/src/HOL/ex/Primes.ML Fri Jul 31 11:03:21 1998 +0200 @@ -10,8 +10,6 @@ eta_contract:=false; -open Primes; - (************************************************) (** Greatest Common Divisor **) (************************************************)