# HG changeset patch
# User wenzelm
# Date 1183494447 -7200
# Node ID e43686246de4cc915956b3d43105e0eb6343b77a
# Parent  0de52773029493ecedcf1f17b56da3b076d25c4a
proper use of ioa_package.ML;

diff -r 0de527730294 -r e43686246de4 src/HOLCF/IOA/ROOT.ML
--- a/src/HOLCF/IOA/ROOT.ML	Tue Jul 03 22:27:25 2007 +0200
+++ b/src/HOLCF/IOA/ROOT.ML	Tue Jul 03 22:27:27 2007 +0200
@@ -2,11 +2,8 @@
     ID:         $Id$
     Author:     Olaf Mueller
 
-This is the ROOT file for the formalization of a semantic model of
-I/O-Automata.  See the README.html file for details.
+Formalization of a semantic model of I/O-Automata.  See README.html
+for details.
 *)
 
-goals_limit := 1;
-
 time_use_thy "meta_theory/Abstraction";
-time_use "meta_theory/ioa_package.ML";
diff -r 0de527730294 -r e43686246de4 src/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Jul 03 22:27:25 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Jul 03 22:27:27 2007 +0200
@@ -7,6 +7,7 @@
 
 theory Abstraction
 imports LiveIOA
+uses ("ioa_package.ML")
 begin
 
 defaultsort type
@@ -639,4 +640,6 @@
 end
 *}
 
+use "ioa_package.ML"
+
 end