src/Tools/isac/Knowledge/Descript.thy
author Walther Neuper <neuper@ist.tugraz.at>
Tue, 05 Oct 2010 09:01:30 +0200
branchisac-update-Isa09-2
changeset 38042 26f3832d96b2
parent 37965 9c11005c33b8
child 41921 d236572c99f2
permissions -rw-r--r--
repaired assoc_thy

such that assoc_thy "Rational" works.
There are related TODOs: fun theory'2thyID, ??
     1 (* Title:  descriptions for items in model-patterns of problems and in method's 
     2            guards
     3    Author: Walther Neuper 000301
     4    (c) due to copyright terms
     5    + see WN, Reactive User-Guidance ... Vers. Oct.2000 p.48 ff
     6 *)
     7 
     8 theory Descript imports Delete begin
     9 
    10 consts
    11 
    12   someList       :: "'a list => unl" (*not for elementwise input, eg. inssort*)
    13 
    14   additionalRels :: "bool list => una"
    15   boundVariable  :: "real => una"
    16 (*derivative     :: 'a => toreal 28.11.00*)
    17   derivative     :: "real => una"
    18   equalities     :: "bool list => tobooll" (*WN071228 see fixedValues*)
    19   equality       :: "bool => una"
    20   errorBound     :: "bool => nam"
    21   
    22   fixedValues    :: "bool list => nam"
    23   functionEq     :: "bool => una"     (*6.5.03: functionTerm -> functionEq*)
    24   antiDerivative :: "bool => una"
    25   functionOf     :: "real => una"
    26 (*functionTerm   :: 'a => toreal 28.11.00*)
    27   functionTerm   :: "real => una"     (*6.5.03: functionTerm -> functionEq*)
    28   interval       :: "real set => una"
    29   maxArgument    :: "bool => toreal"
    30   maximum        :: "real => toreal"
    31   
    32   relations      :: "bool list => una"
    33   solutions      :: "bool list => toreall"
    34 (*solution       :: bool => toreal  WN0509 bool list=> toreall --->EqSystem*)
    35   solveFor       :: "real => una"
    36   differentiateFor:: "real => una"
    37   unknown        :: "'a => unknow"
    38   valuesFor      :: "real list => toreall"
    39 
    40   realTestGiven  :: "real => una"
    41   realTestFind   :: "real => una"
    42   boolTestGiven  :: "bool => una"
    43   boolTestFind   :: "bool => una"
    44 
    45 end