Add AllCasePreds()

[IlmariReissumies]

This is meant to be like AllCaseEqs(), but for the situation where the case statement occurs at the top level.

Yong Kiam threatened he might use every_case_tac if there is no convenient way to do this.

[mn200]

Please add regression tests somewhere to exercise this code. To get your test a fairly rich context, maybe put something into src/boss/theory_tests, where you can see, for example caseEqAbbrevScript.sml.

[mn200]

I'm also a bit leery of repeatedly re-deriving all of the "elim" theorems each time; note how the case_eq theorems are proved once and stored in the TypeBase.

[IlmariReissumies]

I'm also a bit leery of repeatedly re-deriving all of the "elim" theorems each time; note how the case_eq theorems are proved once and stored in the TypeBase.

If you'd prefer storing the theorems in the TypeBase I'm happy to do it like that; I just wasn't sure if it was worth it since this setup wasn't noticeably slow for me. But to be fair I haven't tested it in theories with many datatypes, or with many constructors yet.

[IlmariReissumies]

@mn200 I believe I've addressed all your comments now.

[mn200]

Thanks!