aboutsummaryrefslogtreecommitdiff
path: root/hott/More_List.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/More_List.thy
parentc19533acfad3bbe603cd8a3d176e8b14f477573a (diff)
more reorganizing
Diffstat (limited to 'hott/More_List.thy')
-rw-r--r--hott/More_List.thy8
1 files changed, 8 insertions, 0 deletions
diff --git a/hott/More_List.thy b/hott/More_List.thy
new file mode 100644
index 0000000..2f868b8
--- /dev/null
+++ b/hott/More_List.thy
@@ -0,0 +1,8 @@
+theory More_List
+imports Spartan.List
+
+begin
+
+
+
+end