aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Projections.thy2
-rw-r--r--README.md2
2 files changed, 2 insertions, 2 deletions
diff --git a/Projections.thy b/Projections.thy
index 8ff6b30..1473e08 100644
--- a/Projections.thy
+++ b/Projections.thy
@@ -21,7 +21,7 @@ declare fst_type [intro]
lemma fst_cmp:
assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "fst A <a, b> \<equiv> a"
-unfolding fst_def by compute (derive lems: assms)
+unfolding fst_def by (subst comp) (derive lems: assms)
declare fst_cmp [comp]
diff --git a/README.md b/README.md
index f2a997b..f254a8a 100644
--- a/README.md
+++ b/README.md
@@ -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