diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/Descript.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Knowledge/Descript.thy Wed Aug 25 16:20:07 2010 +0200 @@ -0,0 +1,52 @@ +(* Title: descriptions for items in model-patterns of problems and in method's + guards + Author: Walther Neuper 000301 + (c) due to copyright terms + + see WN, Reactive User-Guidance ... Vers. Oct.2000 p.48 ff + +remove_thy"Descript"; +use_thy"Knowledge/Descript"; +use_thy_only"Knowledge/Descript"; + +remove_thy"Typefix"; +use_thy"Knowledge/Isac"; +*) + +theory Descript imports "../ProgLang/Script" begin + +consts + + someList :: "'a list => unl" (*not for elementwise input, eg. inssort*) + + additionalRels :: "bool list => una" + boundVariable :: "real => una" +(*derivative :: 'a => toreal 28.11.00*) + derivative :: "real => una" + equalities :: "bool list => tobooll" (*WN071228 see fixedValues*) + equality :: "bool => una" + errorBound :: "bool => nam" + + fixedValues :: "bool list => nam" + functionEq :: "bool => una" (*6.5.03: functionTerm -> functionEq*) + antiDerivative :: "bool => una" + functionOf :: "real => una" +(*functionTerm :: 'a => toreal 28.11.00*) + functionTerm :: "real => una" (*6.5.03: functionTerm -> functionEq*) + interval :: "real set => una" + maxArgument :: "bool => toreal" + maximum :: "real => toreal" + + relations :: "bool list => una" + solutions :: "bool list => toreall" +(*solution :: bool => toreal WN0509 bool list=> toreall --->EqSystem*) + solveFor :: "real => una" + differentiateFor:: "real => una" + unknown :: "'a => unknow" + valuesFor :: "real list => toreall" + + realTestGiven :: "real => una" + realTestFind :: "real => una" + boolTestGiven :: "bool => una" + boolTestFind :: "bool => una" + +end \ No newline at end of file