1.1 --- a/src/Tools/isac/Build_Isac.thy	Wed Jan 13 13:55:56 2016 +0100
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Wed Jan 13 14:37:27 2016 +0100
     1.3 @@ -12,13 +12,13 @@
     1.4    for debugging see text at begin (theory dependencies!) *}
     1.5  
     1.6  theory Build_Isac 
     1.7 -imports Complex_Main
     1.8 +imports
     1.9  (* structure inherited from migration which began with Isabelle2009. improve?
    1.10            theory KEStore
    1.11              ML_file "~~/src/Tools/isac/library.sml"
    1.12              ML_file "~~/src/Tools/isac/calcelems.sml"
    1.13          theory ListC 
    1.14 -          imports Complex_Main "~~/src/Tools/isac/KEStore"
    1.15 +          imports "~~/src/Tools/isac/KEStore"
    1.16            ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
    1.17            ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
    1.18            ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"

     2.1 --- a/src/Tools/isac/KEStore.thy	Wed Jan 13 13:55:56 2016 +0100
     2.2 +++ b/src/Tools/isac/KEStore.thy	Wed Jan 13 14:37:27 2016 +0100
     2.3 @@ -3,7 +3,7 @@
     2.4  *)
     2.5  
     2.6  theory KEStore 
     2.7 -imports Complex_Main
     2.8 +imports "~~/src/HOL/Complex_Main"
     2.9  begin
    2.10    ML_file "~~/src/Tools/isac/library.sml"
    2.11    ML_file "~~/src/Tools/isac/calcelems.sml"

     3.1 --- a/src/Tools/isac/Knowledge/Calculus.thy	Wed Jan 13 13:55:56 2016 +0100
     3.2 +++ b/src/Tools/isac/Knowledge/Calculus.thy	Wed Jan 13 14:37:27 2016 +0100
     3.3 @@ -1,3 +1,3 @@
     3.4 -theory Calculus imports Real begin
     3.5 +theory Calculus imports "~~/src/HOL/Real" begin
     3.6  
     3.7  end
     3.8 \ No newline at end of file

     4.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Wed Jan 13 13:55:56 2016 +0100
     4.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Wed Jan 13 14:37:27 2016 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4          10        20        30        40        50        60        70        80         90      100
     4.5  *)
     4.6  
     4.7 -theory GCD_Poly_ML imports Complex_Main begin 
     4.8 +theory GCD_Poly_ML imports Atools begin 
     4.9  
    4.10  text {*
    4.11    Below we reference 

     5.1 --- a/src/Tools/isac/Knowledge/Trig.thy	Wed Jan 13 13:55:56 2016 +0100
     5.2 +++ b/src/Tools/isac/Knowledge/Trig.thy	Wed Jan 13 14:37:27 2016 +0100
     5.3 @@ -1,3 +1,3 @@
     5.4 -theory Trig imports Real begin
     5.5 +theory Trig imports "~~/src/HOL/Real" begin
     5.6  ML {*"test"*}
     5.7  end
     5.8 \ No newline at end of file

     6.1 --- a/src/Tools/isac/Knowledge/Vect.thy	Wed Jan 13 13:55:56 2016 +0100
     6.2 +++ b/src/Tools/isac/Knowledge/Vect.thy	Wed Jan 13 14:37:27 2016 +0100
     6.3 @@ -1,3 +1,3 @@
     6.4 -theory Vect imports Real begin
     6.5 +theory Vect imports "~~/src/HOL/Real" begin
     6.6  
     6.7  end

     7.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Wed Jan 13 13:55:56 2016 +0100
     7.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Wed Jan 13 14:37:27 2016 +0100
     7.3 @@ -4,7 +4,7 @@
     7.4  *)
     7.5  
     7.6  theory ListC 
     7.7 -imports Complex_Main "~~/src/Tools/isac/KEStore"
     7.8 +imports "~~/src/Tools/isac/KEStore"
     7.9  begin
    7.10  
    7.11  ML_file "~~/src/Tools/isac/ProgLang/termC.sml"