diff options
author | Josh Chen | 2020-05-27 21:31:57 +0200 |
---|---|---|
committer | Josh Chen | 2020-05-27 21:31:57 +0200 |
commit | ed41980ed5cee12d7c5eea2e40627e5a390a83f8 (patch) | |
tree | 19b5fbf5a7d8bbec09c9f61c9f74c700b69c52b1 /hott/Identity.thy | |
parent | 62c1c8f306bff84b74b3b1c935d0d6722e1251a2 (diff) |
minor
Diffstat (limited to 'hott/Identity.thy')
-rw-r--r-- | hott/Identity.thy | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/hott/Identity.thy b/hott/Identity.thy index d664fbc..64aea5a 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -145,6 +145,7 @@ Lemma (derive) pathcomp_refl: definition [implicit]: "ru p \<equiv> pathcomp_refl ? ? ? p" definition [implicit]: "lu p \<equiv> refl_pathcomp ? ? ? p" + translations "CONST ru p" \<leftharpoondown> "CONST pathcomp_refl A x y p" "CONST lu p" \<leftharpoondown> "CONST refl_pathcomp A x y p" |