equal
deleted
inserted
replaced
83 |
83 |
84 ML \<open> |
84 ML \<open> |
85 val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false); |
85 val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false); |
86 \<close> |
86 \<close> |
87 |
87 |
|
88 * WN: rewriting with ctxt not complete (cause errors hard to indentify later) |
|
89 - Prconditions.eval |
|
90 - Solve_Step.check ..Rewrite_Inst, Substitute, .. |
|
91 - Error_Pattern.check_for', fill_form |
|
92 - Derive.steps |
|
93 - Fetch_Tacs.specific_from_prog ? |
|
94 - ? LIST IS NOT COMPLETE |
|
95 |
|
96 * WN: ? Rational.Cancel_p; extend use of \<^theory> to \<^theory_context> |
|
97 |
88 * WN: redesign transition from Specification to Solution: how relate |
98 * WN: redesign transition from Specification to Solution: how relate |
89 - Formalise.model with variants (e.g. VSCode_Example) |
99 - Formalise.model with variants (e.g. VSCode_Example) |
90 reconsider separation of variants F_I, F_II, see MAWEN paper |
100 reconsider separation of variants F_I, F_II, see MAWEN paper |
91 - !?! I_Model of MethodC (fairly free sequence, dependent on Formalise.model) |
101 - !?! I_Model of MethodC (fairly free sequence, dependent on Formalise.model) |
92 - !?! formal arguments of program (fixed sequence) |
102 - !?! formal arguments of program (fixed sequence) |