# HG changeset patch
# User wenzelm
# Date 1283529432 -7200
# Node ID dd043196150758e1ee53cd6c7153e2cf1c246086
# Parent  7bfa17bcd5ee531111f59b4dc13143e03b5b3bb5
modernized session ROOT;

diff -r 7bfa17bcd5ee -r dd0431961507 src/HOLCF/IOA/ABP/Correctness.thy
--- 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"
diff -r 7bfa17bcd5ee -r dd0431961507 src/HOLCF/IOA/ABP/ROOT.ML
--- 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"];