Move Definitions into same Tabs as Theorems

[TentativeConvert]

While working on Robo, I noticed that it would make much more sense to have both Definitions and Theorems in Tabs, not just Theorems. For example, I would like to have

• a tab "Logic" with Definitions from logic and Theorems from logic
• a tab "Sets" with Defitionts and Theorems concerning Sets
• a tab "Function" with Definitions and Theorems concerning Functions

etc. At the moment, I'm deliberately leaving many Definitions undocumented so that the Definitions don't take up too much space in the Inventory.

[joneugster]

I'd hope that having three major tabs Tactic/Theorems/Defs as planned would already help with this problem even without having tabs for definitions.

Implementing this would be simple though 👍

[TentativeConvert]

Is “three major tabs Tactic/Theorems/Defs” planned or already implemented in some version? I had a vague memory of that plan, and wrote the issue because I think this alternative might make more sense – at least for from the perspective of Robo. But if “three major tabs” is already implemented, you can close this.

[joneugster]

Implemented in the version which I'm trying to get to a recent Lean.

I'll close issues after I get that version running