1.1 --- a/src/Tools/isac/IsacKnowledge/DiffApp.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,40 +0,0 @@
     1.4 -(* application of differential calculus
     1.5 -   use_thy_only"../IsacKnowledge/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