Boolean decider for primeness implicit in Thm*  !{p:()| x:. p(x)  prime(x) }

	Who Cites prime decider?
prime_decider	Def  is_prime(x) == prime_decider_exists{1:l}(x)
	Thm*  x:. is_prime(x)

Syntax:

is_prime(x)

has structure:

prime_decider(x)

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html