diff options
| author | Josh Chen | 2019-02-23 18:58:20 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-23 18:58:20 +0100 |
| commit | 76a009527d42c9939575f429a406a084c48fe653 (patch) | |
| tree | b047e7e64af6e3c61b7f149031bbe78695a6137b /README.md | |
| parent | 232856fbef15105f619a5c1056da2602984804df (diff) | |
touchups
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -15,7 +15,7 @@ In its current state it is best viewed as a formalization of HoTT within Isabell Work is slowly ongoing to develop the logic into a fully-featured framework in which one can formulate and prove mathematical statements, in the style of the univalent foundations school. While Isabelle has provided support for object logics based on Martin-Löf type theory since the beginning, these have largely been ignored in favor of Isabelle/HOL. -Thus this project is also an experiment in creating a viable framework, based on dependent type theory, inside the simple type theoretic foundations of Isabelle. +Thus this project is also an experiment in creating a viable framework, based on dependent type theory, inside the simple type theoretic foundations of Isabelle/Pure. ### License |