modernized session ROOT;

--- a/src/HOLCF/IOA/ABP/Correctness.thy	Fri Sep 03 17:54:43 2010 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy	Fri Sep 03 17:57:12 2010 +0200
@@ -6,6 +6,7 @@
 
 theory Correctness
 imports IOA Env Impl Impl_finite
+uses "Check.ML"
 begin
 
 primrec reduce :: "'a list => 'a list"

--- a/src/HOLCF/IOA/ABP/ROOT.ML	Fri Sep 03 17:54:43 2010 +0200
+++ b/src/HOLCF/IOA/ABP/ROOT.ML	Fri Sep 03 17:57:12 2010 +0200
@@ -4,5 +4,4 @@
 This is the ROOT file for the Alternating Bit Protocol performed in
 I/O-Automata.
 *)
-use "Check.ML";
 use_thys ["Correctness"];