Adding a method to identify duplicate theorems

[ordinarymath]

Currently there's no easy way to identity theorems. This proposal would consist of warning when proving a theorem if a duplicate theorem already exists.

There's a related zulip discussion. #❄️ HOL4 > Warning when proving duplicate theorems