--- a/src/HOL/HOLCF/IOA/ABP/Read_me Sun Dec 06 13:22:20 2020 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-Isabelle Verification of the Alternating Bit Protocol by
-combining IOA with Model Checking
-
--------------------------------------------------------------
-
-Correctness.ML contains the proof of the abstraction from unbounded
-channels to finite ones.
-
-Check.ML contains a simple ModelChecker prototype checking Spec against
-the finite version of the ABP-protocol.
--- a/src/HOL/ROOT Sun Dec 06 13:22:20 2020 +0100
+++ b/src/HOL/ROOT Sun Dec 06 13:31:42 2020 +0100
@@ -1140,7 +1140,14 @@
description "
Author: Olaf Mueller
- The Alternating Bit Protocol performed in I/O-Automata.
+ The Alternating Bit Protocol performed in I/O-Automata:
+ 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
+ against the finite version of the ABP-protocol.
"
theories
Correctness