# Theory Graph_Theory_Relations

section ‹Graph Theory Inheritance›
text ‹ This theory aims to demonstrate the use of locales to transfer theorems between different
graph/combinatorial structure representations ›
theory Graph_Theory_Relations imports Undirected_Graph_Basics Bipartite_Graphs
"Design_Theory.Block_Designs" "Design_Theory.Group_Divisible_Designs"
begin
subsection ‹ Design Inheritance ›
text ‹A graph is a type of incidence system, and more specifically a type of combinatorial design.
This section demonstrates the correspondence between designs and graphs ›