(* File: Sep_Examples.thy Author: Bohua Zhan Overall directory of examples in Imperative. *) theory Sep_Examples imports GCD_Impl ― ‹Tutorial› ― ‹Inductive data structures› LinkedList ― ‹Linked lists› BST_Impl ― ‹Binary search tree› RBTree_Impl ― ‹Red-black tree› ― ‹Array algorithms› Arrays_Impl ― ‹Standard procedure on arrays› DynamicArray ― ‹Dynamic array› Quicksort_Impl ― ‹Quicksort› Indexed_PQueue_Impl ― ‹Indexed priority queue› Union_Find_Impl ― ‹Union-find› ― ‹Applications› Connectivity_Impl ― ‹Connectivity on graphs› Dijkstra_Impl ― ‹Dijkstra's algorithm› Rect_Intersect_Impl ― ‹Rectangular intersection› begin end