# HG changeset patch
# User wenzelm
# Date 1607257902 -3600
# Node ID fe7df3f7412e64706df04bbe6f34975a78659ba2
# Parent  03803bbfdca35a4ac7157eedb7aac768a56ca8c4
eliminated odd "Read_me";

diff -r 03803bbfdca3 -r fe7df3f7412e src/HOL/HOLCF/IOA/ABP/Read_me
--- 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.
diff -r 03803bbfdca3 -r fe7df3f7412e src/HOL/ROOT
--- 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