1.1 --- a/src/Tools/isac/Build_Isac.thy	Fri Apr 10 14:46:55 2020 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Fri Apr 10 15:02:50 2020 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4    ~$ evince file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf &
     1.5  
     1.6  ATTENTION: no errors in this theory do not mean that there are no errors in Isac ..
     1.7 -.. open theories collecting files from folders: CalcElements.thy, ProgLang.thy etc.
     1.8 +.. open theories collecting files from folders: BaseDefinitions.thy, ProgLang.thy etc.
     1.9  Errors are rigorously detected by isabelle build.
    1.10  *)
    1.11  
    1.12 @@ -25,20 +25,20 @@
    1.13        ML_file "error-fill-def.sml"
    1.14        ML_file "rule-set.sml"
    1.15        ML_file calcelems.sml
    1.16 -  theory CalcElements imports KEStore
    1.17 +  theory BaseDefinitions imports KEStore
    1.18      ML_file termC.sml
    1.19      ML_file contextC.sml
    1.20      ML_file environment.sml
    1.21 -*)        "CalcElements/CalcElements"
    1.22 +*)        "BaseDefinitions/BaseDefinitions"
    1.23  
    1.24 -(*    theory Calculate imports "~~/src/Tools/isac/CalcElements/CalcElements"
    1.25 +(*    theory Calculate imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.26          ML_file calculate.sml
    1.27  
    1.28 -      theory ListC imports "~~/src/Tools/isac/CalcElements/CalcElements"
    1.29 +      theory ListC imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.30      theory Prog_Expr imports Calculate ListC
    1.31 -      theory Program imports "~~/src/Tools/isac/CalcElements/CalcElements"
    1.32 -      theory Prog_Tac imports "~~/src/Tools/isac/CalcElements/CalcElements"
    1.33 -      theory Tactical imports "~~/src/Tools/isac/CalcElements/CalcElements"
    1.34 +      theory Program imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.35 +      theory Prog_Tac imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.36 +      theory Tactical imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.37      theory Auto_Prog imports Program Prog_Tac Tactical begin
    1.38    theory ProgLang imports Prog_Expr Auto_Prog
    1.39  *)        "ProgLang/ProgLang"
    1.40 @@ -61,7 +61,7 @@
    1.41      ML_file calculation.sml
    1.42  *)        "MathEngBasic/MathEngBasic"
    1.43  (*
    1.44 -    theory Input_Descript imports "~~/src/Tools/isac/CalcElements/CalcElements"
    1.45 +    theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.46    theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript
    1.47      ML_file ptyps.sml
    1.48      ML_file generate.sml