(*

 $ cd /usr/local/isabisac/test/Tools/isac/ADDTESTS/file-depend

 $ /usr/local/isabisac/bin/isabelle emacs Build_Test.thy &

 *)

 theory Build_Test imports Complex_Main begin

 use     "0foolibrary.ML"

 use_thy "1language/Foo_Language"

 use     "2interpreter/2foointerpreter.ML"

 (*vvvvvvv can be bypassed with Foo_KnowALL

 use_thy "3knowledge/Foo_Know111"

 use_thy "3knowledge/Foo_Know222"

   ^^^^^^^ can be bypassed with Foo_KnowALL*)

 use_thy "3knowledge/Foo_KnowALL"

 text {* the different theories of knowledge are recognized, Const bar*: *}

 ML {* 

 val trm = Syntax.read_term_global @{theory Foo_Know111} 

   "fooprog (foo111 = bar111)";

 val Const ("Foo_Know111.bar111", _) = foointerpret trm;

 val trm = Syntax.read_term_global @{theory Foo_Know222} 

   "fooprog (foo222 = bar222)";

 val Const ("Foo_Know222.bar222", _) = foointerpret trm;

 *}

 text {* the different theories of knowledge are recognized, Free bar*: *}

 ML {*

 val trm = Syntax.read_term_global @{theory Foo_Know111} 

   "fooprog (foo222 = bar222)";

 (*Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $

      (Const ("op =", "'a => 'a => bool") $ Free ("foo222", "'a") $

        Free ("bar222", "'a"))

    : term*)

 val trm = Syntax.read_term_global @{theory Foo_Know222} 

   "fooprog (foo111 = bar111)";

 (*val trm =

    Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $

      (Const ("op =", "'a => 'a => bool") $ Free ("foo111", "'a") $

        Free ("bar111", "'a"))

    : term*)

 *}