equal
deleted
inserted
replaced
1 (* application of differential calculus |
|
2 use_thy_only"../IsacKnowledge/DiffApp"; |
|
3 use_thy_only"DiffApp"; |
|
4 |
|
5 |
|
6 *) |
|
7 |
|
8 |
|
9 DiffApp = Diff + |
|
10 |
|
11 consts |
|
12 |
|
13 Maximum'_value |
|
14 :: "[bool list,real,bool list,real,real set,bool,\ |
|
15 \ bool list] => bool list" |
|
16 ("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9) |
|
17 |
|
18 Make'_fun'_by'_new'_variable |
|
19 :: "[real,real,bool list, \ |
|
20 \ bool] => bool" |
|
21 ("((Script Make'_fun'_by'_new'_variable (_ _ _ =))// \ |
|
22 \(_))" 9) |
|
23 Make'_fun'_by'_explicit |
|
24 :: "[real,real,bool list, \ |
|
25 \ bool] => bool" |
|
26 ("((Script Make'_fun'_by'_explicit (_ _ _ =))// \ |
|
27 \(_))" 9) |
|
28 |
|
29 dummy :: real |
|
30 |
|
31 (*for script Maximum_value*) |
|
32 filterVar :: "[real, 'a list] => 'a list" |
|
33 |
|
34 (*primrec*)rules |
|
35 filterVar_Nil "filterVar v [] = []" |
|
36 filterVar_Const "filterVar v (x#xs) = \ |
|
37 \(if (v mem (Vars x)) then x#(filterVar v xs) \ |
|
38 \ else filterVar v xs) " |
|
39 |
|
40 end |
|