13 where |
13 where |
14 filterVar_Nil: \<open>filterVar v [] = []\<close> |
14 filterVar_Nil: \<open>filterVar v [] = []\<close> |
15 | filterVar_Const: \<open>filterVar v (x # xs) = |
15 | filterVar_Const: \<open>filterVar v (x # xs) = |
16 (if v \<in> set (Vars x) then x # (filterVar v xs) else filterVar v xs)\<close> |
16 (if v \<in> set (Vars x) then x # (filterVar v xs) else filterVar v xs)\<close> |
17 |
17 |
18 |
|
19 text \<open>WN.6.5.03: old decisions in this file partially are being changed |
|
20 in a quick-and-dirty way to make scripts run: Maximum_value, |
|
21 Make_fun_by_new_variable, Make_fun_by_explicit. |
|
22 found to be reconsidered: |
|
23 - descriptions (Input_Descript.thy) |
|
24 - penv: really need term list; or just rerun the whole example with num/var |
|
25 - mk_arg, arguments_from_model ... env in script different from penv ? |
|
26 - L = SubProblem eq ... show some vars on the worksheet ? (other means for |
|
27 referencing are labels (no on worksheet)) |
|
28 |
|
29 WN.6.5.03 quick-and-dirty: mk_arg, arguments_from_model just make most convenient env |
|
30 from penv as is. |
|
31 \<close> |
|
32 |
18 |
33 ML \<open> |
19 ML \<open> |
34 val eval_rls = prep_rls' ( |
20 val eval_rls = prep_rls' ( |
35 Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI), |
21 Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI), |
36 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [], |
22 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [], |