diff options
| author | Josh Chen | 2019-03-03 22:53:45 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-03-03 22:53:45 +0100 |
| commit | 3f7a8274271b4920e7eccd6f3b4cd516f6c55bd8 (patch) | |
| tree | d2344df927f44e861baeb60c5df43e1b17dcf3fc /Projections.thy | |
| parent | 38dd685f6929d402a32ddfe2d913c7b380b9e935 (diff) | |
Move definition of transport to Type_Families.thy, and change it to use meta-functions for type families again. This together with the previous commit simplifies the definitions and proofs for idtoeqv greatly.
Diffstat (limited to 'Projections.thy')
0 files changed, 0 insertions, 0 deletions