1.1 --- a/src/Tools/isac/Interpret/specification-elems.sml	Sat Jan 21 12:01:30 2017 +0100
     1.2 +++ b/src/Tools/isac/Interpret/specification-elems.sml	Sat Jan 21 12:32:32 2017 +0100
     1.3 @@ -10,7 +10,18 @@
     1.4    datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate
     1.5    val istate2str : istate -> string
     1.6    val e_istate : istate
     1.7 -
     1.8 +  type subs
     1.9 +  type sube
    1.10 +  type subte
    1.11 +  val sube2str : cterm' list -> string
    1.12 +  val sube2subst : theory -> cterm' list -> (term * term) list
    1.13 +  val sube2subte : cterm' list -> term list
    1.14 +  val subs2subst : theory -> cterm' list -> (term * term) list
    1.15 +  val subst2sube : (term * term) list -> cterm' list                       (* for datatypes.sml *)
    1.16 +  val subst2subs : (term * term) list -> cterm' list
    1.17 +  val subst2subs' : (term * term) list -> (string * string) list
    1.18 +  val subte2sube : term list -> cterm' list
    1.19 +  val e_ctxt : Proof.context
    1.20  (*----- needed for tac, tac_ immediately (probably pre-requisites missing)
    1.21    type istate
    1.22    type subte
    1.23 @@ -18,8 +29,12 @@
    1.24    type sube
    1.25  *)
    1.26  (* ---- for tests only: made visible in order to remove the warning --------------------------- *)
    1.27 - val e_fmz : fmz_ * spec                                                  (* for datatypes.sml *)
    1.28 - val scrstate2str : subst * loc_ * term option * term * safe * bool -> string
    1.29 +  val e_fmz : fmz_ * spec                                                  (* for datatypes.sml *)
    1.30 +  val e_sube : cterm' list
    1.31 +  val e_subs : string list
    1.32 +  val scrstate2str : subst * loc_ * term option * term * safe * bool -> string
    1.33 +  val istates2str : istate option * istate option -> string
    1.34 +  val subte2subst : term list -> (term * term) list
    1.35  
    1.36  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.37  
    1.38 @@ -83,4 +98,25 @@
    1.39    | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
    1.40    | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
    1.41  
    1.42 +type subs = cterm' list; (*16.11.00 for FE-KE*)
    1.43 +val e_subs = ["(bdv, x)"]; (* for tests only *)
    1.44 +
    1.45 +(* argument type of tac Rewrite_Inst *)
    1.46 +type sube = cterm' list;
    1.47 +val e_sube = []: cterm' list; (* for tests only *)
    1.48 +fun sube2str s = strs2str s;
    1.49 +
    1.50 +(* _sub_stitution as _t_erms of _e_qualities *)
    1.51 +type subte = term list;
    1.52 +
    1.53 +val subte2sube = map term2str;
    1.54 +val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
    1.55 +fun subst2sube subst = map term2str (map HOLogic.mk_eq subst)
    1.56 +val subst2subs' = map ((apfst term2str) o (apsnd term2str));
    1.57 +fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;
    1.58 +fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;
    1.59 +val sube2subte = map str2term;
    1.60 +val subte2subst = map HOLogic.dest_eq;
    1.61 +val e_ctxt = Proof_Context.init_global @{theory "Pure"};
    1.62 +
    1.63  end