From 76a009527d42c9939575f429a406a084c48fe653 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 23 Feb 2019 18:58:20 +0100 Subject: touchups --- Projections.thy | 2 +- README.md | 2 +- 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 \ U i" and "a: A" and "b: B a" shows "fst A \ 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 -- cgit v1.2.3