src/Tools/isac/calcelems.sml
changeset 59255 383722bfcff5
parent 59253 f0bb15a046ae
child 59257 a1daf71787b1
     1.1 --- a/src/Tools/isac/calcelems.sml	Thu Oct 27 09:53:54 2016 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu Oct 27 10:48:10 2016 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4      by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid.
     1.5    * case 2 "sym_..": Global_Theory.get_thm..RS sym
     1.6    * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_:
     1.7 -    from applicable_in..Calculate: opstr --calculate_/get_calculation_--> (thmID, thm)
     1.8 +    from applicable_in..Calculate: opstr --calculate_/adhoc_thm--> (thmID, thm)
     1.9  *)
    1.10  type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *)
    1.11  type rls' = string;