234 fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') = |
234 fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') = |
235 ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename; |
235 ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename; |
236 |
236 |
237 (**.set up isab_thm_thy in Isac.ML.**) |
237 (**.set up isab_thm_thy in Isac.ML.**) |
238 |
238 |
239 fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, prop_of thm)); |
239 fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, Thm.prop_of thm)); |
240 (* WN120320: reconsider design since thmID and thyID can be retrieved from thm: *) |
240 (* WN120320: reconsider design since thmID and thyID can be retrieved from thm: *) |
241 fun rearrange' (thmID, thm) = |
241 fun rearrange' (thmID, thm) = |
242 (thmID_of_derivation_name thmID, |
242 (thmID_of_derivation_name thmID, |
243 (thyID_of_derivation_name thmID, prop_of thm)): (thmID * (thyID * term)); |
243 (thyID_of_derivation_name thmID, Thm.prop_of thm)): (thmID * (thyID * term)); |
244 fun rearrange_inv (thmID, (thyID, term)) = (thyID, (thmID, term)); |
244 fun rearrange_inv (thmID, (thyID, term)) = (thyID, (thmID, term)); |
245 |
245 |
246 (*================= version before Isbelle2002 --> 2011 =========================== |
246 (*================= version before Isbelle2002 --> 2011 =========================== |
247 (*.lookup the missing theorems in some thy (of Isabelle).*) |
247 (*.lookup the missing theorems in some thy (of Isabelle).*) |
248 fun make_isa missthms thy = |
248 fun make_isa missthms thy = |