diff options
| author | Josh Chen | 2019-03-03 22:47:03 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-03-03 22:48:25 +0100 |
| commit | 38dd685f6929d402a32ddfe2d913c7b380b9e935 (patch) | |
| tree | 8456c696707d90816aef0a6a88db98a873a8fde7 /Type_Families.thy | |
| parent | de6672d6682aea2e7df9e71b2325365dd1383507 (diff) | |
Improve automated handling of universes. derive now can automatically handle more proofs requiring the use of "U i: U (Suc i)", and shouldn't loop as much.
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions