1.1 --- a/src/Tools/isac/Build_Isac.thy	Sat Feb 26 11:34:08 2011 +0100
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Sat Feb 26 12:37:58 2011 +0100
     1.3 @@ -20,8 +20,13 @@
     1.4  header {* Loading the isac mathengine *}
     1.5  
     1.6  theory Build_Isac
     1.7 -(*imports Complex_Main "ProgLang/Language" (*"Knowledge/Isac"*)*)
     1.8 -imports Complex_Main
     1.9 +imports 
    1.10 +  Complex_Main
    1.11 +  "ProgLang/ListC"
    1.12 +  "ProgLang/Tools"
    1.13 +  "ProgLang/Script"
    1.14 +(*"ProgLang/Language"
    1.15 +  "Knowledge/Isac"*)
    1.16  begin
    1.17  
    1.18  ML {* 
    1.19 @@ -37,28 +42,8 @@
    1.20  use "ProgLang/calculate.sml"
    1.21  use "ProgLang/rewrite.sml"
    1.22  
    1.23 -use_thy "ProgLang/ListC_XXX"
    1.24 -ML {* @{thm LENGTH_NIL}*}
    1.25 -
    1.26 -ML {*
    1.27 -val list_rls = 
    1.28 -  Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
    1.29 -      erls = e_rls, srls = Erls, calc = [], (*asm_thm=[],*)
    1.30 -      rules = (*8.01: copied from*)
    1.31 -      [Thm ("refl", num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
    1.32 -       Thm ("o_apply", num_str @{thm o_apply}),
    1.33 -
    1.34 -       Thm ("NTH_CONS",num_str @{thm NTH_CONS})
    1.35 -        ], scr = EmptyScr}:rls;
    1.36 -
    1.37 -*}
    1.38 -ML {*
    1.39 -list_rls;
    1.40 -*}
    1.41 -
    1.42 +use_thy "ProgLang/ListC"
    1.43  use_thy"ProgLang/Tools"
    1.44 -
    1.45 -
    1.46  use_thy"ProgLang/Script"    (*ListC, Tools, Script*)
    1.47  use "ProgLang/scrtools.sml"
    1.48  use_thy"ProgLang/Language"  (*just for integrating scrtools.sml*)

     2.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Sat Feb 26 11:34:08 2011 +0100
     2.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Sat Feb 26 12:37:58 2011 +0100
     2.3 @@ -41,7 +41,6 @@
     2.4    the condition involves another rule set (erls, eval_binop in Atools):*)
     2.5    NTH_CONS:     "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs"
     2.6  
     2.7 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
     2.8  (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
     2.9  (*primrec*)
    2.10    hd_thm:	"hd(x#xs) = x"
    2.11 @@ -198,6 +197,6 @@
    2.12    [("list_rls",list_rls)
    2.13     ]);
    2.14  *}
    2.15 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    2.16  -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    2.17 -
    2.18  end

     3.1 --- a/test/Tools/isac/ADDTESTS/file-depend/1language/Foo_Language.thy	Sat Feb 26 11:34:08 2011 +0100
     3.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/1language/Foo_Language.thy	Sat Feb 26 12:37:58 2011 +0100
     3.3 @@ -1,3 +1,4 @@
     3.4 +(*theory Foo_Language imports Build_Test*)
     3.5  theory Foo_Language imports Complex_Main
     3.6  uses ("../0foolibrary.ML")
     3.7  begin
     3.8 @@ -9,6 +10,5 @@
     3.9  ML {* (* the library function is recognized *)
    3.10    foolibrhs @{term "a = b"}
    3.11  *}
    3.12 -
    3.13  ML {* tracing (PolyML.makestring @{theory}); *}
    3.14  end

     4.1 --- a/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy	Sat Feb 26 11:34:08 2011 +0100
     4.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy	Sat Feb 26 12:37:58 2011 +0100
     4.3 @@ -4,12 +4,15 @@
     4.4  
     4.5  *)
     4.6  
     4.7 -theory Build_Test imports Complex_Main begin
     4.8 +theory Build_Test 
     4.9 +imports 
    4.10 +  Complex_Main 
    4.11 +  "1language/Foo_Language"
    4.12 +  "3knowledge/Foo_KnowALL"
    4.13 +begin
    4.14  
    4.15  use     "0foolibrary.ML"
    4.16  use_thy "1language/Foo_Language"
    4.17 -ML {* @{theory} *}
    4.18 -ML {* @{theory Foo_Language} *}
    4.19  use     "2interpreter/2foointerpreter.ML"
    4.20  
    4.21  (*vvvvvvv can be bypassed with Foo_KnowALL