1.1 --- a/src/Tools/isac/calcelems.sml	Mon Oct 10 18:24:14 2016 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sun Oct 16 13:58:46 2016 +0200
     1.3 @@ -37,6 +37,13 @@
     1.4    Thm.get_name_hint survives num_str and seems perfectly reliable *)
     1.5  
     1.6  type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
     1.7 +(* tricky combination of (string, term) for theorems in Isac:
     1.8 +  * case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm)
     1.9 +    by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid.
    1.10 +  * case 2 "sym_..": Global_Theory.get_thm..RS sym
    1.11 +  * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_:
    1.12 +    from applicable_in..Calculate: opstr --calculate_/get_calculation_--> (thmID, thm)
    1.13 +*)
    1.14  type thm'' = thmID * term; (* only for transport via libisabelle isac-java <--- ME *)
    1.15  type rls' = string;
    1.16