1.1 --- a/src/Tools/isac/CalcElements/calcelems.sml	Tue Aug 27 18:03:33 2019 +0200
     1.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml	Tue Aug 27 18:05:54 2019 +0200
     1.3 @@ -111,11 +111,11 @@
     1.4      val pats2str' : pat list -> string
     1.5      val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list ->
     1.6        thydata ptyp list
     1.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     1.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     1.9      val knowthys: unit -> theory list
    1.10      val e_pbt: pbt
    1.11      val e_met: met
    1.12 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.13 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.14  
    1.15  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    1.16  val overwritelthy: theory -> (Rule.rls' * (string * Rule.rls)) list * (Rule.rls' * Rule.rls) list ->

     2.1 --- a/src/Tools/isac/CalcElements/contextC.sml	Tue Aug 27 18:03:33 2019 +0200
     2.2 +++ b/src/Tools/isac/CalcElements/contextC.sml	Tue Aug 27 18:05:54 2019 +0200
     2.3 @@ -14,9 +14,9 @@
     2.4    val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context
     2.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     2.6    (*NONE*)
     2.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     2.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     2.9    val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
    2.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.12  end
    2.13  
    2.14  (* survey on handling contexts:

     3.1 --- a/src/Tools/isac/CalcElements/libraryC.sml	Tue Aug 27 18:03:33 2019 +0200
     3.2 +++ b/src/Tools/isac/CalcElements/libraryC.sml	Tue Aug 27 18:05:54 2019 +0200
     3.3 @@ -77,10 +77,10 @@
     3.4      val ~~~ : 'a list * 'b list -> ('a * 'b) list
     3.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     3.6      (* NONE *)
     3.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     3.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     3.9      val enumerate_strings: string list -> string list
    3.10      val quad2pair: 'a * 'b * 'c * 'd -> 'a * 'b
    3.11 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    3.12 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    3.13  
    3.14  
    3.15  (*///------------------------------>>> thy ------------------------------------------------\\\*)

     4.1 --- a/src/Tools/isac/CalcElements/rule.sml	Tue Aug 27 18:03:33 2019 +0200
     4.2 +++ b/src/Tools/isac/CalcElements/rule.sml	Tue Aug 27 18:05:54 2019 +0200
     4.3 @@ -110,11 +110,11 @@
     4.4      val terms2str': term list -> string                        (* shift up to Unparse *)
     4.5      val thm2str: thm -> string
     4.6      val thms2str : thm list -> string
     4.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     4.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     4.9      val string_of_thm': theory -> thm -> string                (* shift up to Unparse *)
    4.10      val string_of_thm: thm -> string                           (* shift up to Unparse *)
    4.11      val errpats2str : errpat list -> string
    4.12 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    4.13 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    4.14  
    4.15  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    4.16  

     5.1 --- a/src/Tools/isac/CalcElements/termC.sml	Tue Aug 27 18:03:33 2019 +0200
     5.2 +++ b/src/Tools/isac/CalcElements/termC.sml	Tue Aug 27 18:05:54 2019 +0200
     5.3 @@ -84,10 +84,10 @@
     5.4      val atomty_thy: Rule.thyID -> term -> unit
     5.5      val free2var: term -> term
     5.6      val contains_one_of: thm * (string * typ) list -> bool
     5.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     5.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     5.9      val atomt: term -> unit
    5.10      val typ_a2real: term -> term
    5.11 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    5.12 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    5.13    end
    5.14  
    5.15  (**)

     6.1 --- a/src/Tools/isac/Frontend/interface.sml	Tue Aug 27 18:03:33 2019 +0200
     6.2 +++ b/src/Tools/isac/Frontend/interface.sml	Tue Aug 27 18:05:54 2019 +0200
     6.3 @@ -56,9 +56,9 @@
     6.4      val setNextTactic : Celem.calcID -> Tactic.input -> XML.tree
     6.5      val setProblem : Celem.calcID -> Celem.pblID -> XML.tree
     6.6      val setTheory : Celem.calcID -> Rule.thyID -> XML.tree
     6.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     6.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     6.9      (* NONE *)
    6.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    6.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    6.12    end
    6.13  
    6.14  (**)

     7.1 --- a/src/Tools/isac/Interpret/inform.sml	Tue Aug 27 18:03:33 2019 +0200
     7.2 +++ b/src/Tools/isac/Interpret/inform.sml	Tue Aug 27 18:05:54 2019 +0200
     7.3 @@ -24,7 +24,7 @@
     7.4  
     7.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     7.6    (*  NONE *)
     7.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     7.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     7.9    val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
    7.10    val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
    7.11    val check_err_patt : term * term -> Rule.subst -> Rule.errpatID * term -> Rule.rls -> Rule.errpatID option
    7.12 @@ -32,7 +32,7 @@
    7.13       'a * (term * term) list -> 'b * term -> Rule.errpatID -> Celem.fillpat -> (Celem.fillpatID * term * 'b * 'a) option
    7.14    val get_fillpats :
    7.15       'a * (term * term) list -> term -> Rule.errpatID -> thm -> (Celem.fillpatID * term * thm * 'a) list
    7.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    7.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    7.18  
    7.19  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    7.20    val e_icalhd : icalhd

     8.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Tue Aug 27 18:03:33 2019 +0200
     8.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Tue Aug 27 18:05:54 2019 +0200
     8.3 @@ -40,7 +40,7 @@
     8.4      | NasApp of Istate.scrstate * (Lucin.step list)
     8.5      | NasNap of  term * LTool.env;
     8.6    val assoc2str : assoc -> string
     8.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     8.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     8.9    datatype appy = Appy of Tactic.T * Istate.scrstate | Napp of LTool.env | Skip of term * LTool.env
    8.10    datatype appy_ = Napp_ | Skip_
    8.11    val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
    8.12 @@ -57,7 +57,7 @@
    8.13    val execute_progr_2 : Rule.rls -> Tactic.T -> Ctree.state -> Rule.program * 'a -> Istate.T * Proof.context -> assoc
    8.14    val astep_up : Proof.context * Rule.rls * Rule.program * 'a -> Istate.scrstate * Lucin.step list -> assoc
    8.15    val ass_up : Proof.context * Rule.rls * Rule.program * 'a -> Istate.scrstate * Lucin.step list -> term -> assoc
    8.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    8.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    8.18  end
    8.19  
    8.20  (**)

     9.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Tue Aug 27 18:03:33 2019 +0200
     9.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Tue Aug 27 18:05:54 2019 +0200
     9.3 @@ -28,14 +28,14 @@
     9.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     9.5    val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Tactic.input) * Istate.safe * Ctree.ctree
     9.6    val f2str : Generate.mout -> Rule.cterm'
     9.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     9.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     9.9    type nxt_
    9.10    datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
    9.11    val loc_solve_ : string * Tactic.T -> Ctree.ctree *  Ctree.pos' -> lOc_
    9.12    val loc_specify_ : Tactic.T -> Ctree.state -> lOc_
    9.13    val nxt_specify_: Ctree.ctree * Ctree.pos' -> Chead.calcstate'
    9.14    val TESTg_form : Ctree.state -> Generate.mout
    9.15 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    9.16 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    9.17  
    9.18  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    9.19    (* NONE *)

    10.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Tue Aug 27 18:03:33 2019 +0200
    10.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Tue Aug 27 18:05:54 2019 +0200
    10.3 @@ -45,12 +45,12 @@
    10.4    val guh2theID : Celem.guh -> Celem.theID
    10.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    10.6    (*  NONE *)
    10.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    10.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    10.9    val trtas2str : (term * Rule.rule * (term * term list)) list -> string
   10.10    val eq_Thm : Rule.rule * Rule.rule -> bool
   10.11    val deriv2str : (term * Rule.rule * (term * term list)) list -> string
   10.12    val deriv_of_thm'' : Celem.thm'' -> string
   10.13 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   10.14 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   10.15  
   10.16  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   10.17    val deri2str : (Rule.rule * (term * term list)) list -> string

    11.1 --- a/src/Tools/isac/Interpret/script.sml	Tue Aug 27 18:03:33 2019 +0200
    11.2 +++ b/src/Tools/isac/Interpret/script.sml	Tue Aug 27 18:05:54 2019 +0200
    11.3 @@ -38,11 +38,11 @@
    11.4  
    11.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    11.6    (*NONE*)
    11.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    11.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    11.9    val get_stac : 'a -> term -> term option 
   11.10    val is_spec_pos : Ctree.pos_ -> bool
   11.11    val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
   11.12 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   11.13 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   11.14  
   11.15  end 
   11.16  

    12.1 --- a/src/Tools/isac/Interpret/solve.sml	Tue Aug 27 18:03:33 2019 +0200
    12.2 +++ b/src/Tools/isac/Interpret/solve.sml	Tue Aug 27 18:05:54 2019 +0200
    12.3 @@ -23,9 +23,9 @@
    12.4    val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
    12.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    12.6    val get_form : tac'_ -> Ctree.pos' -> Ctree.ctree -> Generate.mout
    12.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    12.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    12.9    (*NONE*)
   12.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   12.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   12.12  
   12.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   12.14    (* NONE *)

    13.1 --- a/src/Tools/isac/ProgLang/calculate.sml	Tue Aug 27 18:03:33 2019 +0200
    13.2 +++ b/src/Tools/isac/ProgLang/calculate.sml	Tue Aug 27 18:05:54 2019 +0200
    13.3 @@ -16,12 +16,12 @@
    13.4      val popt2str: ('a * term) option -> string
    13.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    13.6    (* NONE *)
    13.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    13.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    13.9      val get_pair: theory -> string -> Rule.eval_fn -> term -> (string * term) option
   13.10      val mk_rule: term list * term * term -> term
   13.11      val divisors: int -> int list
   13.12      val doubles: int list -> int list
   13.13 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   13.14 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   13.15    end
   13.16  
   13.17  (**)

    14.1 --- a/src/Tools/isac/ProgLang/program.sml	Tue Aug 27 18:03:33 2019 +0200
    14.2 +++ b/src/Tools/isac/ProgLang/program.sml	Tue Aug 27 18:05:54 2019 +0200
    14.3 @@ -6,8 +6,8 @@
    14.4  sig
    14.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    14.6    (*NONE*)
    14.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    14.8 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    14.9 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   14.10 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   14.11  end
   14.12  
   14.13  structure Program(**) : PROGRAM(**) =

    15.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Tue Aug 27 18:03:33 2019 +0200
    15.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Tue Aug 27 18:05:54 2019 +0200
    15.3 @@ -23,7 +23,7 @@
    15.4        -> term -> (term * term list) option
    15.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    15.6    (* NONE *)
    15.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    15.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    15.9      val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
   15.10        Rule.rls -> bool -> thm -> term -> (term * term list) option
   15.11      val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule.rls -> term -> (term * term list) option
   15.12 @@ -31,7 +31,7 @@
   15.13      val app_sub: theory -> int -> Rule.rls -> term -> term * term list * bool
   15.14      val mk_thm: theory -> string -> thm
   15.15      val trace1: int -> string -> unit
   15.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   15.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   15.18    end
   15.19  
   15.20  (**)

    16.1 --- a/src/Tools/isac/Specify/appl.sml	Tue Aug 27 18:03:33 2019 +0200
    16.2 +++ b/src/Tools/isac/Specify/appl.sml	Tue Aug 27 18:05:54 2019 +0200
    16.3 @@ -10,9 +10,9 @@
    16.4    val applicable_in : Ctree.pos' -> Ctree.ctree -> Tactic.input -> Chead.appl
    16.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    16.6    val tac2tac_ : Ctree.ctree -> Ctree.pos' -> Tactic.input -> Tactic.T
    16.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    16.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    16.9    val mk_set : 'a -> ctree -> pos -> term -> term -> term * term list
   16.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   16.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   16.12  end
   16.13  
   16.14  (**)

    17.1 --- a/src/Tools/isac/Specify/calchead.sml	Tue Aug 27 18:03:33 2019 +0200
    17.2 +++ b/src/Tools/isac/Specify/calchead.sml	Tue Aug 27 18:05:54 2019 +0200
    17.3 @@ -106,7 +106,7 @@
    17.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    17.5    val e_calcstate : Ctree.state * Generate.taci list
    17.6    val e_calcstate' : calcstate'
    17.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    17.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    17.9    val posterms2str : (pos' * term * 'a) list -> string
   17.10    val postermtacs2str : (pos' * term * Tactic.input option) list -> string
   17.11    val vals_of_oris : Model.ori list -> term list
   17.12 @@ -124,7 +124,7 @@
   17.13      Model.itm list -> (string * (term * term)) list -> Rule.cterm' -> additm
   17.14    val nxt_add: theory -> (int * int list * string * term * term list) list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
   17.15    val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
   17.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   17.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   17.18  
   17.19  (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
   17.20    val variants_in : term list -> int

    18.1 --- a/src/Tools/isac/Specify/ctree-access.sml	Tue Aug 27 18:03:33 2019 +0200
    18.2 +++ b/src/Tools/isac/Specify/ctree-access.sml	Tue Aug 27 18:05:54 2019 +0200
    18.3 @@ -38,12 +38,12 @@
    18.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    18.5    val cappend_parent : CTbasic.ctree -> int list -> Istate.T * Proof.context -> term ->
    18.6      Tactic.input -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list
    18.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    18.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    18.9    val update_loc' : CTbasic.ctree -> CTbasic.pos ->
   18.10      (Istate.T * Proof.context) option * (Istate.T * Proof.context) option -> CTbasic.ctree
   18.11    val append_problem : int list -> Istate.T * Proof.context -> Selem.fmz ->
   18.12      Model.ori list * Celem.spec * term -> CTbasic.ctree -> CTbasic.ctree
   18.13 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   18.14 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   18.15  end
   18.16  (**)
   18.17  structure CTaccess(**): CALC_TREE_ACCESS(**) =

    19.1 --- a/src/Tools/isac/Specify/ctree-basic.sml	Tue Aug 27 18:03:33 2019 +0200
    19.2 +++ b/src/Tools/isac/Specify/ctree-basic.sml	Tue Aug 27 18:05:54 2019 +0200
    19.3 @@ -112,7 +112,7 @@
    19.4    val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos   (* duplicate in ctree-navi.sml *)
    19.5     ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
    19.6  
    19.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    19.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    19.9    val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
   19.10    val pr_short : pos -> ppobj -> string
   19.11    val g_ctxt : ppobj -> Proof.context
   19.12 @@ -126,7 +126,7 @@
   19.13    val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
   19.14    val get_trace : ctree -> int list -> int list -> int list list
   19.15    val branch2str : branch -> string
   19.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   19.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   19.18  
   19.19  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   19.20    (* NONE *)

    20.1 --- a/src/Tools/isac/Specify/ctree-navi.sml	Tue Aug 27 18:03:33 2019 +0200
    20.2 +++ b/src/Tools/isac/Specify/ctree-navi.sml	Tue Aug 27 18:05:54 2019 +0200
    20.3 @@ -28,9 +28,9 @@
    20.4  
    20.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    20.6    (* NONE *)
    20.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    20.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    20.9    (* NONE *)
   20.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   20.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   20.12  
   20.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   20.14    (* NONE *)

    21.1 --- a/src/Tools/isac/Specify/ctree.sml	Tue Aug 27 18:03:33 2019 +0200
    21.2 +++ b/src/Tools/isac/Specify/ctree.sml	Tue Aug 27 18:05:54 2019 +0200
    21.3 @@ -15,9 +15,9 @@
    21.4    open CTnavi
    21.5    open CTaccess
    21.6  end;
    21.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    21.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    21.9    open Ctree;
   21.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   21.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   21.12  
   21.13  (* policy for "open" structures:
   21.14  --------------------------------

    22.1 --- a/src/Tools/isac/Specify/generate.sml	Tue Aug 27 18:03:33 2019 +0200
    22.2 +++ b/src/Tools/isac/Specify/generate.sml	Tue Aug 27 18:05:54 2019 +0200
    22.3 @@ -30,9 +30,9 @@
    22.4      Ctree.pos' -> Ctree.ctree -> Ctree.state (* for interface.sml *)
    22.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    22.6    val tacis2str : taci list -> string
    22.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    22.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    22.9    (*  NONE *)
   22.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   22.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   22.12  
   22.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   22.14    (* NONE *)

    23.1 --- a/src/Tools/isac/Specify/mstools.sml	Tue Aug 27 18:03:33 2019 +0200
    23.2 +++ b/src/Tools/isac/Specify/mstools.sml	Tue Aug 27 18:05:54 2019 +0200
    23.3 @@ -20,9 +20,9 @@
    23.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    23.5    val pres2str : (bool * term) list -> string
    23.6    val refined : match list -> Celem.pblID
    23.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    23.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    23.9    (*NONE*)
   23.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   23.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   23.12  
   23.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   23.14    val pblID_of_match : match -> Celem.pblID

    24.1 --- a/src/Tools/isac/Specify/ptyps.sml	Tue Aug 27 18:03:33 2019 +0200
    24.2 +++ b/src/Tools/isac/Specify/ptyps.sml	Tue Aug 27 18:05:54 2019 +0200
    24.3 @@ -55,14 +55,14 @@
    24.4    val e_errpat : Rule.errpat
    24.5    val show_pblguhs : unit -> unit
    24.6    val sort_pblguhs : unit -> unit
    24.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    24.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    24.9    val add_field : theory -> Celem.pat list -> term * 'b -> string * term * 'b
   24.10    val add_variants : ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
   24.11    val coll_variants: ('a * ''b) list -> ('a list * ''b) list
   24.12    val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
   24.13    val max: int list -> int
   24.14    val replace_0: int -> int list -> int list
   24.15 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   24.16 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   24.17  
   24.18  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   24.19    val e_fillpat : string * term * string

    25.1 --- a/src/Tools/isac/Specify/specification-elems.sml	Tue Aug 27 18:03:33 2019 +0200
    25.2 +++ b/src/Tools/isac/Specify/specification-elems.sml	Tue Aug 27 18:05:54 2019 +0200
    25.3 @@ -33,9 +33,9 @@
    25.4    val e_sube : Rule.cterm' list
    25.5    val e_subs : string list
    25.6    val subte2subst : term list -> (term * term) list
    25.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    25.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    25.9    (*  NONE *)
   25.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   25.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   25.12  
   25.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   25.14  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)

    26.1 --- a/src/Tools/isac/Specify/tactic.sml	Tue Aug 27 18:03:33 2019 +0200
    26.2 +++ b/src/Tools/isac/Specify/tactic.sml	Tue Aug 27 18:05:54 2019 +0200
    26.3 @@ -112,9 +112,9 @@
    26.4    val rule2tac : theory -> (term * term) list ->  Rule.rule -> input         (* for rewtools.sml *)
    26.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    26.6    (* NONE *)
    26.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    26.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    26.9    (* NONE *)
   26.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   26.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   26.12  
   26.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   26.14    (* NONE *)