1.1 --- a/src/Tools/isac/Interpret/specification-elems.sml	Wed Dec 12 19:52:53 2018 +0100
     1.2 +++ b/src/Tools/isac/Interpret/specification-elems.sml	Fri Dec 14 18:46:04 2018 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4    type subs
     1.5    type sube
     1.6    type subte
     1.7 +  val subst'_to_sube : term -> Rule.cterm' list
     1.8    val sube2str : Rule.cterm' list -> string
     1.9    val sube2subst : theory -> Rule.cterm' list -> (term * term) list
    1.10    val sube2subte : Rule.cterm' list -> term list
    1.11 @@ -118,6 +119,14 @@
    1.12  (* _sub_stitution as _t_erms of _e_qualities *)
    1.13  type subte = term list;
    1.14  
    1.15 +type subst' = term (* decomposes to "(char list * term) list", where term is Free ("xxx", _)
    1.16 +  e.g. @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"} *)
    1.17 +fun subst'_to_sube sub = sub 
    1.18 +  |> HOLogic.dest_list 
    1.19 +  |> map HOLogic.dest_prod 
    1.20 +  |> map (fn (e1, e2) => (HOLogic.dest_string e1, Rule.term2str e2))
    1.21 +  |> map (fn (e1, e2) => "(" ^ e1 ^ ", " ^ e2 ^ ")"): Rule.cterm' list
    1.22 +
    1.23  val subte2sube = map Rule.term2str;
    1.24  val subst2subs = map (pair2str o (apfst Rule.term2str) o (apsnd Rule.term2str));
    1.25  fun subst2sube subst = map Rule.term2str (map HOLogic.mk_eq subst)

     2.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Wed Dec 12 19:52:53 2018 +0100
     2.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Fri Dec 14 18:46:04 2018 +0100
     2.3 @@ -30,7 +30,7 @@
     2.4    Differentiate  :: "[bool * real] => bool"
     2.5  
     2.6    (*subproblem and script-name*)
     2.7 -  differentiate  :: "[ID * (ID list) * ID, real,real] => real"
     2.8 +  differentiate  :: "[char list * char list list * char list, real, real] => real"
     2.9                 	   ("(differentiate (_)/ (_ _ ))" 9)
    2.10    DiffScr        :: "[real,real,  real] => real"
    2.11                     ("((Script DiffScr (_ _ =))// (_))" 9)

     3.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Wed Dec 12 19:52:53 2018 +0100
     3.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Fri Dec 14 18:46:04 2018 +0100
     3.3 @@ -130,10 +130,8 @@
     3.4  remdups_Nil:	"remdups [] = []" and
     3.5  remdups_Cons:	"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 
     3.6  
     3.7 -(** Lexicographic orderings on lists ...!!!**)
     3.8 -
     3.9 -ML\<open>(*the former ListC.ML*)
    3.10 -(** rule set for evaluating listexpr in scripts **)
    3.11 +ML\<open>
    3.12 +(** rule set for evaluating listexpr in scripts, will be extended in several thys **)
    3.13  val list_rls = 
    3.14    Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 
    3.15      erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],

     4.1 --- a/src/Tools/isac/ProgLang/Script.thy	Wed Dec 12 19:52:53 2018 +0100
     4.2 +++ b/src/Tools/isac/ProgLang/Script.thy	Fri Dec 14 18:46:04 2018 +0100
     4.3 @@ -39,7 +39,6 @@
     4.4    Substitute   :: "[bool list, 'a] => 'a"
     4.5  
     4.6    Map          :: "['a => 'b, 'a list] => 'b list"
     4.7 -  Tac          :: "ID => 'a"         (*deprecated; used in Test.ML*)
     4.8    Check'_elementwise ::
     4.9  		  "['a list, 'b set] => 'a list"
    4.10                                       ("Check'_elementwise (_ _)" 11)