(* Title: HOL/IOA/ABP/ROOT.ML ID: $Id$ Author: Olaf Müller License: GPL (GNU GENERAL PUBLIC LICENSE) This is the ROOT file for the Alternating Bit Protocol performed in I/O-Automata. *) goals_limit := 1; time_use_thy "Correctness";