(* Title: HOLCF/IOA/ABP/ROOT.ML Author: Olaf Mueller This is the ROOT file for the Alternating Bit Protocol performed in I/O-Automata. *) goals_limit := 1; use "Check.ML"; use_thys ["Correctness"];