aboutsummaryrefslogtreecommitdiff
path: root/ex
diff options
context:
space:
mode:
authorJosh Chen2018-09-18 21:20:08 +0200
committerJosh Chen2018-09-18 21:20:08 +0200
commit59a1409b1d15860344e91a4512b60ab8d4368e44 (patch)
treefe25a144dfac0727a71371176d3f63927407d2d9 /ex
parentc93932c689640a530de946f35a0a9dc82e56e776 (diff)
parentf9bbcffd4a45599c306815104dccb6b549b306ee (diff)
Merge branch 'larsrh-topic/root'
Diffstat (limited to 'ex')
-rw-r--r--ex/Book/Ch1.thy (renamed from ex/HoTT book/Ch1.thy)2
1 files changed, 1 insertions, 1 deletions
diff --git a/ex/HoTT book/Ch1.thy b/ex/Book/Ch1.thy
index 263f43d..dfb1879 100644
--- a/ex/HoTT book/Ch1.thy
+++ b/ex/Book/Ch1.thy
@@ -1,5 +1,5 @@
(*
-Title: ex/HoTT book/Ch1.thy
+Title: ex/Book/Ch1.thy
Author: Josh Chen
Date: 2018