The Nuprl 5 system has autonomous components such as the Common Mathematics Library, the resident and external editors, and various refiners (logic engines) such as Jason Hickey's MetaPRL system.
