equal
deleted
inserted
replaced
67 Thus eliminate use of Thy_Info.get_theory |
67 Thus eliminate use of Thy_Info.get_theory |
68 follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__" |
68 follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__" |
69 |
69 |
70 * WN: improve naming in refine.sml, m-match.sml |
70 * WN: improve naming in refine.sml, m-match.sml |
71 * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store› |
71 * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store› |
|
72 * WN: review Prog_Tac: |
|
73 (*+isa==isa2*)@{term "Substitution []"}; (*Free ("Subproblem",.. ALSO Subproblem, ?!*) |
|
74 (*+isa==isa2*)@{term "Rewrite_Set ''norm_Rational''"}; (*Const ("Prog_Tac.Rewrite_Set",..*) |
72 * WN: KEStore_Elems.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes: |
75 * WN: KEStore_Elems.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes: |
73 (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys |
76 (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys |
74 (2) Error_Pattern.fill_in stored with thm (in thes): instead introduce new Thy_Data for them. |
77 (2) Error_Pattern.fill_in stored with thm (in thes): instead introduce new Thy_Data for them. |
75 adapt KEStore_Elems.insert_fillpats for that purpose. |
78 adapt KEStore_Elems.insert_fillpats for that purpose. |
76 |
79 |