Provide default names that indicate the "interpretation" of each cell

[kim-em]

Currently new cells receive default names Cell n. This could be changed to produce Generator n (if created using target), or Definition n/Proof n (if created using theorem).

This would indicate to the user the "natural interpretation" of the cells when the system is thought of as an interactive theorem prover. The fact that these interpretations were only shown in the "meaningless" user-facing name might ensure the user doesn't mistakenly come to believe that the different types of cells actually behave any differently during the rest of the interaction.

[alexarice]

I like the idea of giving a different name to proofs. Would you call both 0-cells made with the plus button and cells made with source/target generators? I am not sure this gains much over calling them cells. For theorems I would suggest that the theorem statement be called theorem n and it's proof be called proof n