| changeset 9826 | 5b5d9ee742ca |
| parent 9747 | 043098ba5098 |
| child 9870 | 2374ba026fc6 |
--- a/src/HOL/ex/Factorization.ML Mon Sep 04 10:25:32 2000 +0200 +++ b/src/HOL/ex/Factorization.ML Mon Sep 04 10:26:34 2000 +0200 @@ -6,6 +6,9 @@ Fundamental Theorem of Arithmetic (unique factorization into primes) *) +val prime_def = thm "prime_def"; +val prime_dvd_mult = thm "prime_dvd_mult"; + (* --- Arithmetic --- *)