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"