wneuper/isa: src/Tools/isac/BaseDefinitions/celem-7.sml@68396aa5821f

     1 (* Title:  BaseDefinitions/celem-7.sml

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     5           *)

     6 signature CALCELEMENT_7 =

     7 (*/------- to Celem7 -------\*)

     8 (*\------- to Celem7 -------/*)

     9 sig

    10 (*/------- to Celem7 -------\*)

    11   type cas_elem

    12   val cas_eq: cas_elem * cas_elem -> bool

    13 (*\------- to Celem7 -------/*)

    14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

    15   (*NONE*)

    16 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

    17   (*NONE*)

    18 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

    19 end

    21 (**)

    22 structure Celem7(**): CALCELEMENT_7(**) =

    23 struct

    24 (**)

    26 (*/------- to Celem7 -------\*)

    27 (* association list with cas-commands, for generating a complete calc-head *)

    28 type generate_fn =

    29   (term list ->    (* the arguments of the cas-command, eg. (x+1=2, x) *)

    30     (term *        (* description of an element                        *)

    31       term list)   (* value of the element (always put into a list)    *)

    32   list)            (* of elements in the formalization                 *)

    33 type cas_elem =

    34   (term *          (* cas-command, eg. 'solve'                         *)

    35     (Spec.spec *        (* theory, problem, method                          *)

    36     generate_fn))

    37 fun cas_eq ((t1, (_, _)) : cas_elem, (t2, (_, _)) : cas_elem) = t1 = t2

    38 (*\------- to Celem7 -------/*)

    40 (**)end(**)

author	Walther Neuper <walther.neuper@jku.at>
	Sun, 19 Apr 2020 16:43:53 +0200
changeset 59891	68396aa5821f
parent 59886	106e7d8723ca
permissions	-rw-r--r--