Thanks to previous responses and to Dan, Mark, Mike and Tom ... a good set of contributions. I was asking the question because I was thinking about a database of theorems, showing - individual theorems as a set of initial 'constraints' leading to a 'result', but also - showing how other theorems are used to produce the new theorem. The 'graph' of these theorems is not a hierarchy or even a lattice ... but theorem-equivalences show that it is a more general graph. Has anyone produced this kind of database of theorems on a computer - with access-software, GUI etc?! I guess 'Principia Mathematica' was a first demonstration, pre computer. Somewhere well downstream, we get to '1 + 1 = 2' with the footnote "The above proposition is occasionally useful." Thank again - Guy