1.1 --- a/src/Tools/isac/Knowledge/Diff_App.thy	Sat Aug 26 15:14:24 2023 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Diff_App.thy	Sun Aug 27 11:19:14 2023 +0200
     1.3 @@ -16,20 +16,6 @@
     1.4        (if v \<in> set (Vars x) then x # (filterVar v xs) else filterVar v xs)\<close>
     1.5  
     1.6  
     1.7 -text \<open>WN.6.5.03: old decisions in this file partially are being changed
     1.8 -  in a quick-and-dirty way to make scripts run: Maximum_value,
     1.9 -  Make_fun_by_new_variable, Make_fun_by_explicit.
    1.10 -found to be reconsidered:
    1.11 -- descriptions (Input_Descript.thy)
    1.12 -- penv: really need term list; or just rerun the whole example with num/var
    1.13 -- mk_arg, arguments_from_model ... env in script different from penv ?
    1.14 -- L = SubProblem eq ... show some vars on the worksheet ? (other means for
    1.15 -  referencing are labels (no on worksheet))
    1.16 -
    1.17 -WN.6.5.03 quick-and-dirty: mk_arg, arguments_from_model just make most convenient env
    1.18 -  from penv as is.    
    1.19 -\<close>
    1.20 -
    1.21  ML \<open>
    1.22  val eval_rls = prep_rls' (
    1.23    Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),