1.1 --- a/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 11:07:02 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 12:22:37 2020 +0200
1.3 @@ -73,7 +73,7 @@
1.4 TODO (d1) lookup from calctxt
1.5 TODO (d1) lookup from from rule set in MiniBrowser *)
1.6 type thehier = (thydata Celem1.ptyp) list;
1.7 -(* required to determine sequence of main nodes of thehier in KEStore.thy *)
1.8 +(* required to determine sequence of main nodes of thehier in Know_Store.thy *)
1.9 fun part2guh [str] = (case str of
1.10 "Isabelle" => "thy_isab_" ^ str ^ "-part" : Celem2.guh
1.11 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"