src/Tools/isac/BaseDefinitions/celem-7.sml
changeset 59893 3479b100fbcc
parent 59892 b8cfae027755
child 59894 b9e10434530c
     1.1 --- a/src/Tools/isac/BaseDefinitions/celem-7.sml	Mon Apr 20 15:54:19 2020 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,40 +0,0 @@
     1.4 -(* Title:  BaseDefinitions/celem-7.sml
     1.5 -   Author: Walther Neuper
     1.6 -   (c) due to copyright terms
     1.7 -
     1.8 -          *)
     1.9 -signature CALCELEMENT_7 =
    1.10 -(*/------- to Celem7 -------\*)
    1.11 -(*\------- to Celem7 -------/*)
    1.12 -sig
    1.13 -(*/------- to Celem7 -------\*)
    1.14 -  type cas_elem
    1.15 -  val cas_eq: cas_elem * cas_elem -> bool
    1.16 -(*\------- to Celem7 -------/*)
    1.17 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.18 -  (*NONE*)
    1.19 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.20 -  (*NONE*)
    1.21 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.22 -end
    1.23 -
    1.24 -(**)
    1.25 -structure Celem7(**): CALCELEMENT_7(**) =
    1.26 -struct
    1.27 -(**)
    1.28 -
    1.29 -(*/------- to Celem7 -------\*)
    1.30 -(* association list with cas-commands, for generating a complete calc-head *)
    1.31 -type generate_fn = 
    1.32 -  (term list ->    (* the arguments of the cas-command, eg. (x+1=2, x) *)
    1.33 -    (term *        (* description of an element                        *)
    1.34 -      term list)   (* value of the element (always put into a list)    *)
    1.35 -  list)            (* of elements in the formalization                 *)
    1.36 -type cas_elem = 
    1.37 -  (term *          (* cas-command, eg. 'solve'                         *)
    1.38 -    (Spec.spec *        (* theory, problem, method                          *)
    1.39 -    generate_fn))
    1.40 -fun cas_eq ((t1, (_, _)) : cas_elem, (t2, (_, _)) : cas_elem) = t1 = t2
    1.41 -(*\------- to Celem7 -------/*)
    1.42 -
    1.43 -(**)end(**)