IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Sharing Formal Mathematics

Here we discuss how two systems implementing formal logics might share theorems, proofs, or definitions. These are general methodological rather than technical considerations.

The Form of the Problem

The form of the problem we consider is how to produce a candidate for a proof in a "recipient" system that borrows results from a "donor" system, and how one would argue for the result's correctness in the recipient's logic. We use "logic" in a sense that two systems can share a common logic but with some different primitives, including axioms. A logic in this sense characterizes not a specific class of theorems or inferences but rather proof structure. When multiple systems serve as mutual donors we would have a hybrid system proper.

We approach the problem from two directions: the Forms of Sharing Math and What Math can be Shared.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html