1.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Fri Jan 06 10:33:16 2023 +0100
     1.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Fri Jan 06 10:50:33 2023 +0100
     1.3 @@ -10,7 +10,6 @@
     1.4    imports "$ISABELLE_ISAC/Test_Code/Test_Code"
     1.5  begin
     1.6    ML_file "pbl-met-hierarchy.sml" (*keep as a model for browsing pbl and met hierarchies*)
     1.7 -  ML_file "thy-hierarchy.sml"     (*replace by Isabelle/PIDE*)
     1.8    ML_file "present-tool.sml"      (*keep tests of interaction Java-frontend <-> Kernel running*)
     1.9    ML_file mathml.sml              (*keep tests of interaction Java-frontend <-> Kernel running*)
    1.10    ML_file datatypes.sml           (*keep tests of interaction Java-frontend <-> Kernel running*)

     2.1 --- a/src/Tools/isac/Interpret/Interpret.thy	Fri Jan 06 10:33:16 2023 +0100
     2.2 +++ b/src/Tools/isac/Interpret/Interpret.thy	Fri Jan 06 10:50:33 2023 +0100
     2.3 @@ -9,7 +9,6 @@
     2.4  imports Specify.Specify
     2.5  begin
     2.6    ML_file istate.sml
     2.7 -  ML_file "thy-read.sml"
     2.8    ML_file "li-tool.sml"
     2.9    ML_file "solve-step.sml"
    2.10    ML_file "error-pattern.sml"

     3.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Fri Jan 06 10:33:16 2023 +0100
     3.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Fri Jan 06 10:50:33 2023 +0100
     3.3 @@ -73,9 +73,9 @@
     3.4  \<close>
     3.5  
     3.6  subsubsection \<open>From rule-sets collect theorems, which have been taken from Isabelle\<close>
     3.7 -ML \<open>
     3.8 +text \<open>
     3.9    val isacrlsthms =                      (*length = 460*)
    3.10 -    Thy_Hierarchy.thms_of_rlss @{theory} (Know_Store.get_rlss knowledge_parent) : ThmC.T list
    3.11 +    Thy_Hierarchy.thms_of_rlss @ {theory} (Know_Store.get_rlss knowledge_parent) : ThmC.T list
    3.12  
    3.13    val rlsthmsNOTisac = isacrlsthms       (*length =  36*)
    3.14      |> filter (fn (deriv, _) => 
    3.15 @@ -97,7 +97,7 @@
    3.16    ==============================================================================================
    3.17    See "etc/preferences".
    3.18  \<close>
    3.19 -ML \<open>
    3.20 +text \<open>
    3.21  val thydata_list = (* SEE NOTE ABOVE *)
    3.22    Thy_Hierarchy.collect_part       "IsacKnowledge" knowledge_parent knowthys' @
    3.23    (map (Thy_Hierarchy.collect_isab "Isabelle") rlsthmsNOTisac) @
    3.24 @@ -112,9 +112,9 @@
    3.25    collect_part       "IsacKnowledge" knowledge_parent knowthys'
    3.26  \<close> ML \<open>
    3.27  "~~~~~ fun collect_part , args:"; val (part, parent, thys) = ("IsacKnowledge", knowledge_parent, knowthys');
    3.28 -\<close> ML \<open>
    3.29 +\<close> text \<open>
    3.30      val xxx = (flat (map (Thy_Hierarchy.collect_thms part) thys))
    3.31 -\<close> ML \<open>
    3.32 +\<close> text \<open>
    3.33  val 34 = length thys;
    3.34  val 479 = length xxx;
    3.35  \<close> text \<open>
    3.36 @@ -128,8 +128,9 @@
    3.37     =============================== works =========================================================
    3.38  *)
    3.39  Know_Store.get_rlss parent
    3.40 +
    3.41 +setup \<open>Know_Store.add_thes (map (fn (a, b) => (b, a)) thydata_list)\<close>
    3.42  \<close>
    3.43 -setup \<open>Know_Store.add_thes (map (fn (a, b) => (b, a)) thydata_list)\<close>
    3.44  
    3.45  
    3.46  section \<open>interface for dialog-authoring\<close>