aboutsummaryrefslogtreecommitdiff
path: root/HoTT.thy
blob: 405364e1542601b47529a2367f2cee8efd2d9590 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
(*  Title:  HoTT/HoTT.thy
    Author: Josh Chen

Load all the component modules for the HoTT logic.
*)

theory HoTT imports
  HoTT_Base
  Prod Sum

begin

\<comment> \<open>Maybe tactic setup can go in here?\<close>

end