src/HOLCF/IOA/meta_theory/Abstraction.thy

 
 header {* Abstraction Theory -- tailored for I/O automata *}
 
 theory Abstraction
 imports LiveIOA
+uses ("ioa_package.ML")
 begin
 
 defaultsort type
 
 consts

       auto_tac (cs addSIs weak_strength_lemmas,
         ss addsimps [state_strengthening_def, state_weakening_def]))) i
 end
 *}
 
+use "ioa_package.ML"
+
 end