(* 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