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