diff options
author | Josh Chen | 2018-08-18 16:18:23 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-18 16:18:23 +0200 |
commit | 03c734ea067bd28210530d862137133e2215ca80 (patch) | |
tree | 3e21b040d84af0337abecd7d6db2a530764c144b | |
parent | a1603ffdddcbe333a3e4f0f328a4c25698c2d475 (diff) |
HoTT_Test.thy should go in test/
-rw-r--r-- | tests/Test.thy (renamed from HoTT_Test.thy) | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/HoTT_Test.thy b/tests/Test.thy index da044b4..433039c 100644 --- a/HoTT_Test.thy +++ b/tests/Test.thy @@ -1,4 +1,4 @@ -(* Title: HoTT/HoTT_Test.thy +(* Title: HoTT/tests/Test.thy Author: Josh Chen Date: Aug 2018 |