equal
deleted
inserted
replaced
420 if hd id = "#" |
420 if hd id = "#" |
421 then mk_thm thy ct' |
421 then mk_thm thy ct' |
422 else thmid |> convert_metaview_to_thmid thy |> num_str |
422 else thmid |> convert_metaview_to_thmid thy |> num_str |
423 ) handle _ (*TODO: fin exn behind ERROR: Undefined fact: "add_commute"*) => |
423 ) handle _ (*TODO: fin exn behind ERROR: Undefined fact: "add_commute"*) => |
424 error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)") |
424 error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)") |
425 (*> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_#mult_2_3","6 = 2 * 3"); |
|
426 val it = "6 = 2 * 3" : thm |
|
427 |
|
428 > assoc_thm' (Thy_Info.get_theory "Isac") ("add_0_left",""); |
|
429 val it = "0 + ?z = ?z" : thm |
|
430 |
|
431 > assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left",""); |
|
432 val it = "?t = 0 + ?t" [.] : thm |
|
433 |
|
434 > assoc_thm' @{theory HOL} ("sym_real_add_zero_left",""); |
|
435 *** Unknown theorem(s) "add_0_left" |
|
436 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents) |
|
437 uncaught exception ERROR*) |
|
438 |
|
439 |
425 |
440 fun parse' (thy:theory') (ct:cterm') = |
426 fun parse' (thy:theory') (ct:cterm') = |
441 case parse (assoc_thy thy) ct of |
427 case parse (assoc_thy thy) ct of |
442 NONE => NONE |
428 NONE => NONE |
443 | SOME ct => SOME ((term2str (term_of ct)):cterm'); |
429 | SOME ct => SOME ((term2str (term_of ct)):cterm'); |