src/HOL/ROOT

     combining IOA with Model Checking.
 
     Theory Correctness contains the proof of the abstraction from unbounded
     channels to finite ones.
 
-    Fole Check.ML contains a simple ModelChecker prototype checking Spec
+    File Check.ML contains a simple ModelChecker prototype checking Spec
     against the finite version of the ABP-protocol.
   "
   theories
     Correctness
     Spec