diff options
author | Josh Chen | 2018-06-18 11:20:11 +0200 |
---|---|---|
committer | Josh Chen | 2018-06-18 11:20:11 +0200 |
commit | 912a4a4b909041cb280ae5cecd40867ce34b58de (patch) | |
tree | 1e998ccd205e692ba2c9eea3497acd58c2b3aa10 /HoTT_Base.thy | |
parent | f88e1c0de030ac32014dd6f4f04fb4c6961b93ab (diff) |
Removed all [simp] attributes, these will be added later when I set up the simplifier. Proved simplification rule for dependent fst.
Diffstat (limited to '')
-rw-r--r-- | HoTT_Base.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 9b7c3e2..7794601 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -34,7 +34,7 @@ consts is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ :/ _)" [0, 0] 1000) axiomatization where - inhabited_implies_type: "\<And>a A. a : A \<Longrightarrow> A : U" + inhabited_implies_type [intro]: "\<And>a A. a : A \<Longrightarrow> A : U" section \<open>Type families\<close> |