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;