equal
deleted
inserted
replaced
486 end; |
486 end; |
487 |
487 |
488 |
488 |
489 (**** retrieve the axioms that were used in the proof ****) |
489 (**** retrieve the axioms that were used in the proof ****) |
490 |
490 |
491 (*PureThy.get_name_hint returns "??.unknown" if no name is available.*) |
491 (*Thm.get_name_hint returns "??.unknown" if no name is available.*) |
492 fun goodhint x = (x <> "??.unknown"); |
492 fun goodhint x = (x <> "??.unknown"); |
493 |
493 |
494 (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*) |
494 (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*) |
495 fun get_axiom_names (thm_names: string vector) step_nums = |
495 fun get_axiom_names (thm_names: string vector) step_nums = |
496 let fun is_axiom n = n <= Vector.length thm_names |
496 let fun is_axiom n = n <= Vector.length thm_names |