Theory Busy_Beaver

theory Busy_Beaver
  imports
    Busy_Beaver_Base
    Turing_Busy_Beaver
begin

section ‹The Busy Beaver Entry›

text ‹
  This theory is the AFP entry point.  It collects the abstract Busy Beaver
  upper-bound principle and its instantiation for the Turing machines from the
  AFP Universal Turing Machine development.
›

end