1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,40 @@
     1.4 +(* application of differential calculus
     1.5 +   use_thy_only"../Knowledge/DiffApp";
     1.6 +   use_thy_only"DiffApp";
     1.7 +   
     1.8 +
     1.9 +*)
    1.10 +
    1.11 +
    1.12 +DiffApp = Diff +
    1.13 +
    1.14 +consts
    1.15 +
    1.16 +  Maximum'_value
    1.17 +             :: "[bool list,real,bool list,real,real set,bool,\
    1.18 +		  \ bool list] => bool list"
    1.19 +               ("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9)
    1.20 +  
    1.21 +  Make'_fun'_by'_new'_variable
    1.22 +             :: "[real,real,bool list, \
    1.23 +		  \ bool] => bool"
    1.24 +               ("((Script Make'_fun'_by'_new'_variable (_ _ _ =))// \
    1.25 +		  \(_))" 9)
    1.26 +  Make'_fun'_by'_explicit
    1.27 +             :: "[real,real,bool list, \
    1.28 +		  \ bool] => bool"
    1.29 +               ("((Script Make'_fun'_by'_explicit (_ _ _ =))// \
    1.30 +		  \(_))" 9)
    1.31 +
    1.32 +  dummy :: real
    1.33 +
    1.34 +(*for script Maximum_value*)
    1.35 +  filterVar :: "[real, 'a list] => 'a list"
    1.36 +
    1.37 +(*primrec*)rules
    1.38 +  filterVar_Nil		"filterVar v []     = []"
    1.39 +  filterVar_Const	"filterVar v (x#xs) =                      \
    1.40 +			\(if (v mem (Vars x)) then x#(filterVar v xs) \
    1.41 +			\                   else filterVar v xs)   "
    1.42 +
    1.43 +end
    1.44 \ No newline at end of file