src/Tools/isac/calcelems.sml
changeset 55485 b10eb9fd4c02
parent 55483 066b35da6c97
child 55487 06883b595617
     1.1 --- a/src/Tools/isac/calcelems.sml	Mon Jul 28 17:06:16 2014 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu Jul 31 14:15:41 2014 +0200
     1.3 @@ -536,7 +536,8 @@
     1.4  
     1.5  (* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
     1.6  TODO (a): thehier does not contain sym_thmID theorems
     1.7 -TODO (b): lookup to thehier for sym_thmID creates response using sym_thm
     1.8 +     (b): lookup for sym_thmID directly from Isabelle using sym_thm
     1.9 +          (within math-engine NO lookup in thehier -- within java in *.xml only!)
    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"