src/HOL/HOLCF/IOA/ABP/ROOT.ML
author bulwahn
Thu, 05 May 2011 10:47:31 +0200
changeset 42695 a94ad372b2f5
parent 42151 4da4fc77664b
permissions -rw-r--r--
adding creation of exhaustive generators for records; simplifying dependencies in Main theory

(*  Title:      HOL/HOLCF/IOA/ABP/ROOT.ML
    Author:     Olaf Mueller

This is the ROOT file for the Alternating Bit Protocol performed in
I/O-Automata.
*)

use_thys ["Correctness"];