equal
deleted
inserted
replaced
63 ***** priority of WN items is top down, most urgent/simple on top |
63 ***** priority of WN items is top down, most urgent/simple on top |
64 |
64 |
65 * WN: follow up 6: eliminate use of Thy_Info.get_theory |
65 * WN: follow up 6: eliminate use of Thy_Info.get_theory |
66 follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__" |
66 follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__" |
67 |
67 |
|
68 * WN: cleanup Problem/MethodC..prep_input |
68 * WN: Sub_Problem.tac_from_prog: use ctxt from pt |
69 * WN: Sub_Problem.tac_from_prog: use ctxt from pt |
69 * WN: improve naming in refine.sml, m-match.sml |
70 * WN: improve naming in refine.sml, m-match.sml |
70 * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store› |
71 * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store› |
71 * WN: review Prog_Tac: |
72 * WN: review Prog_Tac: |
72 (*+isa==isa2*)@{term "Substitution []"}; (*Free ("Subproblem",.. ALSO Subproblem, ?!*) |
73 (*+isa==isa2*)@{term "Substitution []"}; (*Free ("Subproblem",.. ALSO Subproblem, ?!*) |