42 by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid. |
42 by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid. |
43 * case 2 "sym_..": Global_Theory.get_thm..RS sym |
43 * case 2 "sym_..": Global_Theory.get_thm..RS sym |
44 * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_: |
44 * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_: |
45 from applicable_in..Calculate: opstr --calculate_/get_calculation_--> (thmID, thm) |
45 from applicable_in..Calculate: opstr --calculate_/get_calculation_--> (thmID, thm) |
46 *) |
46 *) |
47 type thm'' = thmID * term; (* only for transport via libisabelle isac-java <--- ME *) |
47 type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *) |
48 type rls' = string; |
48 type rls' = string; |
49 |
49 |
50 (*.a 'guh'='globally unique handle' is a string unique for each element |
50 (*.a 'guh'='globally unique handle' is a string unique for each element |
51 of isac's KEStore and persistent over time |
51 of isac's KEStore and persistent over time |
52 (in particular under shifts within the respective hierarchy); |
52 (in particular under shifts within the respective hierarchy); |
291 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); |
291 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); |
292 |
292 |
293 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); |
293 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); |
294 fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm |
294 fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm |
295 fun thyID_of_derivation_name dn = hd (space_explode "." dn); |
295 fun thyID_of_derivation_name dn = hd (space_explode "." dn); |
296 fun thm''_of_thm thm = (thmID_of_derivation_name' thm, Thm.prop_of thm) : thm'' |
296 fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm'' |
297 |
297 |
298 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) = |
298 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) = |
299 (strip_thy thmid1) = (strip_thy thmid2); |
299 (strip_thy thmid1) = (strip_thy thmid2); |
300 (*WN120201 weakened*) |
300 (*WN120201 weakened*) |
301 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _)) = thmid1 = thmid2; |
301 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _)) = thmid1 = thmid2; |