Isabelle-HoTT/ex, branch master trying to make Isabelle/HoTT work with Isabelle 2021-1 https://stuebinm.eu/git/Isabelle-HoTT/atom/ex?h=master 2020-04-02T15:57:48Z Brand-spanking new version using Spartan infrastructure 2020-04-02T15:57:48Z Josh Chen 2020-04-02T15:57:48Z urn:sha1:c2dfffffb7586662c67e44a2d255a1a97ab0398b add ROOT file 2018-09-18T14:52:08Z Lars Hupel 2018-09-18T14:52:08Z urn:sha1:f07e0e2349a222130209ada9c029eea3d1fe8144 Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0! 2018-09-18T09:38:54Z Josh Chen 2018-09-18T09:38:54Z urn:sha1:6857e783fa5cb91f058be322a18fb9ea583f2aad Should write the correct rule for Ord_leq_min. Another exercise. 2018-08-29T22:51:48Z Josh Chen 2018-08-29T22:51:48Z urn:sha1:2a2e8e46e0de6f99154a9421f75ae802557f22c7 Reorganize methods 2018-08-18T21:27:25Z Josh Chen 2018-08-18T21:27:25Z urn:sha1:8833cdf99d3128466d85eb88aeb8e340e07e937c Regrouping type rules 2018-08-18T19:28:21Z Josh Chen 2018-08-18T19:28:21Z urn:sha1:e1be5f97bb2a42b3179bc24b118d69af137f8e5d Misc formatting 2018-08-18T12:34:08Z Josh Chen 2018-08-18T12:34:08Z urn:sha1:41f13f91d023e497d9b35e7a958a961aa0c7a5e5 Some comments and reorganization 2018-08-16T14:28:50Z Josh Chen 2018-08-16T14:28:50Z urn:sha1:d8699451025a3bd5e8955e07fa879ed248418949 Prod.thy now has the correct definitional equality structure rule. Definition of function composition and properties. 2018-08-16T14:13:33Z Josh Chen 2018-08-16T14:11:42Z urn:sha1:8ed9cf8682c07fc47b86c2d0aaeb8b4628aeaa31 Basic compute method 2018-08-15T10:42:52Z Josh Chen 2018-08-15T10:42:52Z urn:sha1:257561ff4036d0eb5b51e649f2590b61e08d6fc5