1.1 --- a/src/Tools/isac/calcelems.sml	Sat Jul 26 14:10:05 2014 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sat Jul 26 14:26:54 2014 +0200
     1.3 @@ -534,6 +534,16 @@
     1.4    | the2str (Hord {guh, coursedesign, mathauthors, ord}) = guh
     1.5  fun thes2str thes = map the2str thes |> list2str;
     1.6  
     1.7 +(* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
     1.8 +TODO (a): thehier does not contain sym_thmID theorems
     1.9 +TODO (b): lookup to thehier for sym_thmID creates response using sym_thm
    1.10 +TODO (c): export from thehier to xml
    1.11 +TODO (c1)   creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy
    1.12 +TODO (c2)   creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"
    1.13 +TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml)
    1.14 +          stands for both, "thmID" and "sym_thmID" 
    1.15 +TODO (d1)   lookup from calctxt          
    1.16 +TODO (d1)   lookup from from rule set in MiniBrowser *)
    1.17  type thehier = (thydata ptyp) list;
    1.18  (* required to determine sequence of main nodes of thehier in KEStore.thy *)
    1.19  fun part2guh ([str]:theID) =