1.1 --- a/src/Tools/isac/Build_Isac.thy	Mon Oct 05 12:05:10 2020 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Mon Oct 05 12:16:16 2020 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4      ML_file substitution.sml
     1.5      ML_file contextC.sml
     1.6      ML_file environment.sml
     1.7 -*)        "BaseDefinitions/BaseDefinitions"
     1.8 +( ** )    "BaseDefinitions/BaseDefinitions"( **)
     1.9  
    1.10  (*    theory Calculate imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.11          ML_file evaluate.sml
    1.12 @@ -50,7 +50,7 @@
    1.13        theory Tactical imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.14      theory Auto_Prog imports Program Prog_Tac Tactical begin
    1.15    theory ProgLang imports Prog_Expr Auto_Prog
    1.16 -*)        "ProgLang/ProgLang"
    1.17 +( ** )    "ProgLang/ProgLang"( **)
    1.18  (*
    1.19    theory MathEngBasic imports
    1.20      "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
    1.21 @@ -77,7 +77,7 @@
    1.22    
    1.23      ML_file "state-steps.sml"
    1.24      ML_file calculation.sml
    1.25 -*)        "MathEngBasic/MathEngBasic"
    1.26 +( ** )    "MathEngBasic/MathEngBasic"( **)
    1.27  (*
    1.28      theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
    1.29    theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript
    1.30 @@ -96,7 +96,7 @@
    1.31      ML_file "input-calchead.sml"
    1.32      ML_file "step-specify.sml"
    1.33      ML_file specify.sml
    1.34 -*)        "Specify/Specify"
    1.35 +( ** )    "Specify/Specify"( **)
    1.36  (*
    1.37    theory Interpret imports "~~/src/Tools/isac/Specify/Specify"
    1.38      ML_file istate.sml
    1.39 @@ -108,9 +108,9 @@
    1.40      ML_file "li-tool.sml"
    1.41      ML_file "lucas-interpreter.sml"
    1.42      ML_file "step-solve.sml"
    1.43 -*)        "Interpret/Interpret"
    1.44 +( ** )    "Interpret/Interpret"( **)
    1.45  (*
    1.46 -  theory MathEngine imports "~~/src/Tools/isac/Interpret/Interpret"
    1.47 +  theory MathEngine imports Interpret.Interpret
    1.48      ML_file "fetch-tactics.sml"
    1.49      ML_file solve.sml
    1.50      ML_file step.sml
    1.51 @@ -118,11 +118,11 @@
    1.52      ML_file "mathengine-stateless.sml"
    1.53      ML_file messages.sml
    1.54      ML_file states.sml
    1.55 -*)        "MathEngine/MathEngine"
    1.56 +( ** )    "MathEngine/MathEngine"( **)
    1.57  (*
    1.58    theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine"
    1.59      ML_file "test-code.sml"
    1.60 -*)        "Test_Code/Test_Code"
    1.61 +( ** )    "Test_Code/Test_Code"( **)
    1.62  (*
    1.63    theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine"
    1.64      ML_file "thy-present.sml"
    1.65 @@ -132,12 +132,12 @@
    1.66      ML_file "thy-hierarchy.sml" 
    1.67      ML_file "interface-xml.sml"
    1.68      ML_file interface.sml
    1.69 -*)        "BridgeLibisabelle/BridgeLibisabelle"
    1.70 +( ** )    "BridgeLibisabelle/BridgeLibisabelle"( **)
    1.71  (*
    1.72      theory Isac imports  "~~/src/Tools/isac/MathEngine/MathEngine"
    1.73        ML_file parseC.sml
    1.74    theory BridgeJEdit imports Isac    
    1.75 -*)        "BridgeJEdit/BridgeJEdit"
    1.76 +( ** )    "BridgeJEdit/BridgeJEdit"( **)
    1.77  
    1.78            "Knowledge/Build_Thydata" (*imports Isac.thy etc*)
    1.79  
    1.80 @@ -167,7 +167,7 @@
    1.81                                                           
    1.82  ML \<open>Prog_Expr.eval_occurs_in\<close>
    1.83  ML \<open>@{thm last_thmI}\<close>
    1.84 -ML \<open>@{thm Querkraft_Belastung}\<close>
    1.85 +(** )ML \<open>@{thm Querkraft_Belastung}\<close>( *exception FAIL NONE raised (line 161 of "General/scan.ML")*)
    1.86  
    1.87  ML \<open>Check_Unique.on := false;\<close>
    1.88  ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>