changeset 61032 | b57df8eecad6 |
parent 58880 | 0baae4311a9f |
child 61999 | 89291b5d0ede |
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Thu Aug 27 13:07:45 2015 +0200 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Thu Aug 27 21:19:48 2015 +0200 @@ -5,7 +5,7 @@ section {* The main correctness proof: System_fin implements System *} theory Correctness -imports IOA Env Impl Impl_finite +imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Env Impl Impl_finite begin ML_file "Check.ML"