src/Tools/isac/MathEngBasic/specification-def.sml
changeset 59977 e635534c5f63
child 59985 9aaeab7d38b6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/MathEngBasic/specification-def.sml	Thu May 14 13:33:47 2020 +0200
     1.3 @@ -0,0 +1,34 @@
     1.4 +(* Title:  MathEngBasic/specification-def.sml
     1.5 +   Author: Walther Neuper
     1.6 +   (c) due to copyright terms
     1.7 +
     1.8 +Required for Ctree definition.
     1.9 +*)
    1.10 +signature SPECIFICATION_DEFINITION =
    1.11 +sig
    1.12 +  type T
    1.13 +  val empty: T
    1.14 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.15 +  (*NONE*)
    1.16 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.17 +  (*NONE*)
    1.18 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.19 +
    1.20 +end
    1.21 +
    1.22 +(**)                   
    1.23 +structure Specification_Def(**): SPECIFICATION_DEFINITION(**) =
    1.24 +struct
    1.25 +(**)
    1.26 +
    1.27 +type T =
    1.28 +  bool *              (* I_Model.T andalso Pre_Conds.T      *)
    1.29 +  Pos.pos_ *          (* model belongs to Problem or Method *)
    1.30 +  term *              (* the headline shown on Calc.T       *)
    1.31 +  Model_Def.i_model * (* used by I_Model.T                  *)
    1.32 +  (Pre_Conds_Def.T) * (* used by Pre_Conds.T                *)
    1.33 +  References.T;       (* into Know_Store                    *)
    1.34 +val empty =
    1.35 +  (false, Pos.Und, TermC.empty, [Model_Def.i_model_empty], [(false, TermC.empty)], References.empty);
    1.36 +
    1.37 +(**)end(**)