534 | the2str (Hord {guh, coursedesign, mathauthors, ord}) = guh |
534 | the2str (Hord {guh, coursedesign, mathauthors, ord}) = guh |
535 fun thes2str thes = map the2str thes |> list2str; |
535 fun thes2str thes = map the2str thes |> list2str; |
536 |
536 |
537 (* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting) |
537 (* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting) |
538 TODO (a): thehier does not contain sym_thmID theorems |
538 TODO (a): thehier does not contain sym_thmID theorems |
539 TODO (b): lookup to thehier for sym_thmID creates response using sym_thm |
539 (b): lookup for sym_thmID directly from Isabelle using sym_thm |
|
540 (within math-engine NO lookup in thehier -- within java in *.xml only!) |
540 TODO (c): export from thehier to xml |
541 TODO (c): export from thehier to xml |
541 TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy |
542 TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy |
542 TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml" |
543 TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml" |
543 TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml) |
544 TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml) |
544 stands for both, "thmID" and "sym_thmID" |
545 stands for both, "thmID" and "sym_thmID" |