wneuper/isa: src/Tools/isac/Knowledge/DiffApp.thy@22235e4dbe5f

     1 (* application of differential calculus

     2    use_thy_only"../Knowledge/DiffApp";

     3    use_thy_only"DiffApp";

     6 *)

     9 DiffApp = Diff +

    11 consts

    13   Maximum'_value

    14              :: "[bool list,real,bool list,real,real set,bool,\

    15 		  \ bool list] => bool list"

    16                ("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9)

    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)

    29   dummy :: real

    31 (*for script Maximum_value*)

    32   filterVar :: "[real, 'a list] => 'a list"

    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)   "

    40 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 25 Aug 2010 16:20:07 +0200
branch	isac-update-Isa09-2
changeset 37947	22235e4dbe5f
parent 37906	src/Tools/isac/IsacKnowledge/DiffApp.thy@e2b23ba9df13
child 37954	4022d670753c
permissions	-rw-r--r--