# HG changeset patch # User wenzelm # Date 1224189862 -7200 # Node ID 1f301440c97be9d9427d56f68dbb821d25ed5cc8 # Parent 15a41d3fa959ed9a45bb294f9685dd4dfebb2017 avoid CRITICAL with_path; diff -r 15a41d3fa959 -r 1f301440c97b src/HOLCF/IOA/Modelcheck/MuIOA.thy --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Oct 16 19:44:36 2008 +0200 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Oct 16 22:44:22 2008 +0200 @@ -2,7 +2,7 @@ (* $Id$ *) theory MuIOA -imports IOA MuckeSyn +imports IOA "../../../HOL/Modelcheck/MuckeSyn" begin consts diff -r 15a41d3fa959 -r 1f301440c97b src/HOLCF/IOA/Modelcheck/ROOT.ML --- a/src/HOLCF/IOA/Modelcheck/ROOT.ML Thu Oct 16 19:44:36 2008 +0200 +++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML Thu Oct 16 22:44:22 2008 +0200 @@ -5,7 +5,7 @@ Modelchecker setup for I/O automata. *) -with_path "../../../HOL/Modelcheck" time_use_thy "MuIOAOracle"; +time_use_thy "MuIOAOracle"; (*check if user has mucke installed*) fun mucke_enabled () = getenv "MUCKE_HOME" <> "";