self_destruct : string -> unit
# needs "Library/prime.ml";; ... # let primes_1000 = rev(rev_itlist (fun q ps -> if exists (fun p -> q mod p = 0) ps then ps else q::ps) (2--1000) []);; ...
self_destruct "Preloaded with prime number material";;
$ mv hol.snapshot hol.prime
$ hol.prime HOL Light 2.10, built 16 March 2006 on OCaml 3.08.3 Preloaded with prime number material val it : unit = () #
# PRIME_DIVPROD;; val it : thm = |- !p a b. prime p /\ p divides a * b ==> p divides a \/ p divides b # el 100 primes_1000;; val it : int = 547