equal
deleted
inserted
replaced
29 filterVar :: "[real, 'a list] => 'a list" |
29 filterVar :: "[real, 'a list] => 'a list" |
30 |
30 |
31 (*primrec*)axioms |
31 (*primrec*)axioms |
32 filterVar_Nil: "filterVar v [] = []" |
32 filterVar_Nil: "filterVar v [] = []" |
33 filterVar_Const: "filterVar v (x#xs) = |
33 filterVar_Const: "filterVar v (x#xs) = |
34 (if (v mem (Vars x)) then x#(filterVar v xs) |
34 (if (v : set (Vars x)) then x#(filterVar v xs) |
35 else filterVar v xs) " |
35 else filterVar v xs) " |
36 text {*WN.6.5.03: old decisions in this file partially are being changed |
36 text {*WN.6.5.03: old decisions in this file partially are being changed |
37 in a quick-and-dirty way to make scripts run: Maximum_value, |
37 in a quick-and-dirty way to make scripts run: Maximum_value, |
38 Make_fun_by_new_variable, Make_fun_by_explicit. |
38 Make_fun_by_new_variable, Make_fun_by_explicit. |
39 found to be reconsidered: |
39 found to be reconsidered: |