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>

     2.1 --- a/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy	Mon Oct 05 12:05:10 2020 +0200
     2.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy	Mon Oct 05 12:16:16 2020 +0200
     2.3 @@ -3,7 +3,7 @@
     2.4  (*partially copied from
     2.5    ~/material/texts/emat/lucin-isa/paper-isabisac/Lucin_Isa_IJCAR.thy *)
     2.6  theory Lucas_Interpreter
     2.7 -  imports "~~/src/Tools/isac/Interpret/Interpret"
     2.8 +  imports "Interpret.Interpret"
     2.9  begin
    2.10  ML \<open>
    2.11    open LI

     3.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Oct 05 12:05:10 2020 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Oct 05 12:16:16 2020 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  theory Base_Tools
     3.5 -  imports  "../ProgLang/ProgLang" "../Interpret/Interpret" "../BridgeLibisabelle/BridgeLibisabelle"
     3.6 -                                                          (*  ^^^ for KEStore_Elems.add_thes *)
     3.7 +  imports  Interpret.Interpret "../BridgeLibisabelle/BridgeLibisabelle"
     3.8 +                                (*  ^^^ for KEStore_Elems.add_thes *)
     3.9  begin
    3.10  subsection \<open>theorems for Base_Tools\<close>
    3.11  axiomatization where (*for evaluating the assumptions of conditional rules*)
    3.12 @@ -146,4 +146,4 @@
    3.13  setup \<open>KEStore_Elems.add_rlss
    3.14    [("prog_expr", (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} prog_expr))]\<close>
    3.15  
    3.16 -end
    3.17 \ No newline at end of file
    3.18 +end

     4.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Oct 05 12:05:10 2020 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Oct 05 12:16:16 2020 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4  
     4.5  theory Build_Thydata
     4.6  imports 
     4.7 -  Isac_Knowledge "~~/src/Tools/isac/Interpret/Interpret"
     4.8 +  Isac_Knowledge Interpret.Interpret
     4.9    Test_Build_Thydata (*for test/../build_thydata.sml, thy_hierarchy.sml*)
    4.10  begin
    4.11  

     5.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Mon Oct 05 12:05:10 2020 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Mon Oct 05 12:16:16 2020 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -theory InsSort imports "../Interpret/Interpret" Rational(*for norm_Rational?!?*)
     5.5 +theory InsSort imports "Interpret.Interpret" Rational(*for norm_Rational?!?*)
     5.6  begin
     5.7  
     5.8  section \<open>consts\<close>

     6.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Mon Oct 05 12:05:10 2020 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Mon Oct 05 12:16:16 2020 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  (* Minimal Thydata for test/../thy-hierarchy *)
     6.5  
     6.6  theory Test_Build_Thydata
     6.7 -imports "~~/src/Tools/isac/ProgLang/ProgLang"
     6.8 +  imports "Interpret.ProgLang"
     6.9  begin
    6.10  
    6.11  ML \<open>

     7.1 --- a/src/Tools/isac/MathEngine/MathEngine.thy	Mon Oct 05 12:05:10 2020 +0200
     7.2 +++ b/src/Tools/isac/MathEngine/MathEngine.thy	Mon Oct 05 12:16:16 2020 +0200
     7.3 @@ -4,7 +4,7 @@
     7.4   *)
     7.5  
     7.6  theory MathEngine
     7.7 -  imports "~~/src/Tools/isac/Interpret/Interpret"
     7.8 +  imports Interpret.Interpret
     7.9  begin
    7.10    ML_file "me-misc.sml"
    7.11    ML_file "fetch-tactics.sml"

     8.1 --- a/src/Tools/isac/ROOT	Mon Oct 05 12:05:10 2020 +0200
     8.2 +++ b/src/Tools/isac/ROOT	Mon Oct 05 12:16:16 2020 +0200
     8.3 @@ -10,28 +10,54 @@
     8.4  # this creates, among others:
     8.5  # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
     8.6  *)
     8.7 -(*-------------------------------------------------------
     8.8 -(* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
     8.9 -session Interpret = HOL +
    8.10 -  description \<open>
    8.11 -    Session Isac restricted to code required for paper
    8.12 -    "Lucas-Interpretation on Isabelle’s Functions".
    8.13 -    A first step towards formally checked documentation.
    8.14 -  \<close>
    8.15 +
    8.16 +(* run "./bin/isabelle build -v -b Interpret" *)
    8.17 +session Interpret in Interpret = HOL +
    8.18 +  description "
    8.19 +    Session covering code required for ~~/src/Tools/isac/Doc.
    8.20 +  "
    8.21    options [document = false (*, browser_info = true*)]
    8.22 +  directories
    8.23 +    "../BaseDefinitions"
    8.24 +    "../ProgLang"
    8.25 +    "../MathEngBasic"
    8.26 +    "../Specify"
    8.27    theories
    8.28 -    "Interpret/Interpret"
    8.29 --------------------------------------------------------*)
    8.30 +    "../BaseDefinitions/BaseDefinitions"
    8.31 +    "../ProgLang/ProgLang"
    8.32 +    "../MathEngBasic/MathEngBasic"
    8.33 +    "../Specify/Specify"
    8.34 +    "Interpret"
    8.35 +
    8.36  (* run "./bin/isabelle build -v -b Isac" *)
    8.37 -session Isac = HOL +
    8.38 -  description \<open>
    8.39 +session Isac = Interpret +
    8.40 +  description "
    8.41      Isac core, prototype of a math-engine and knowledge 
    8.42      for a TP-based educational mathematics assistant.
    8.43 +  "
    8.44 +  options [document = false (*, browser_info = true*)]
    8.45 +  directories
    8.46 +    "MathEngine"
    8.47 +    "Test_Code"
    8.48 +    "BridgeLibisabelle"
    8.49 +    "BridgeJEdit"
    8.50 +    "Knowledge"
    8.51 +  theories
    8.52 +    "MathEngine/MathEngine"
    8.53 +    "Test_Code/Test_Code"
    8.54 +    "BridgeLibisabelle/BridgeLibisabelle"
    8.55 +    "BridgeJEdit/BridgeJEdit"
    8.56 +    "Knowledge/Build_Thydata"
    8.57 +    "Build_Isac"
    8.58  
    8.59 -    The java front-end is under development at FH Hagenberg,
    8.60 -    the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
    8.61 -    See http://www.ist.tugraz.at/isac/.
    8.62 -  \<close>
    8.63 +(* run "./bin/isabelle build -v -b Doc" *)
    8.64 +session Doc in Doc = Interpret +
    8.65 +  description "
    8.66 +    Formally checked documentation for Isac in analogy to ~~/Doc/.
    8.67 +  "
    8.68    options [document = false (*, browser_info = true*)]
    8.69 +  directories
    8.70 +    "Lucas_Interpreter"
    8.71    theories
    8.72 -    Build_Isac
    8.73 +    "Lucas_Interpreter/Lucas_Interpreter"
    8.74 +