aboutsummaryrefslogtreecommitdiff
path: root/hott/Nat.thy
diff options
context:
space:
mode:
authorJosh Chen2020-05-25 19:37:57 +0200
committerJosh Chen2020-05-25 19:37:57 +0200
commiteee7d9771c3acd4a45ece85fd9a0bf8f7a46e0e7 (patch)
treeaf91d4d6635ccf65ac6bd7a89f799892cbe6963b /hott/Nat.thy
parentc19533acfad3bbe603cd8a3d176e8b14f477573a (diff)
more reorganizing
Diffstat (limited to '')
-rw-r--r--hott/Nat.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy
index e129be0..d54ea7b 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -1,5 +1,5 @@
theory Nat
-imports Equivalence
+imports Identity
begin