src/Tools/isac/BaseDefinitions/celem-8.sml
changeset 59887 4616b145b1cd
parent 59886 106e7d8723ca
child 59888 2c2fdf9dd52d
     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"