1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml	Thu Nov 14 12:00:13 2019 +0100
     1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml	Thu Nov 14 12:08:05 2019 +0100
     1.3 @@ -56,9 +56,9 @@
     1.4      val setNextTactic : Celem.calcID -> Tactic.input -> XML.tree
     1.5      val setProblem : Celem.calcID -> Celem.pblID -> XML.tree
     1.6      val setTheory : Celem.calcID -> Rule.thyID -> XML.tree
     1.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     1.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     1.9      (* NONE *)
    1.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.12    end
    1.13  
    1.14  (**)

     2.1 --- a/src/Tools/isac/CalcElements/calcelems.sml	Thu Nov 14 12:00:13 2019 +0100
     2.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml	Thu Nov 14 12:08:05 2019 +0100
     2.3 @@ -110,11 +110,11 @@
     2.4      val pats2str' : pat list -> string
     2.5      val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list ->
     2.6        thydata ptyp list
     2.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     2.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     2.9      val knowthys: unit -> theory list
    2.10      val e_pbt: pbt
    2.11      val e_met: met
    2.12 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.13 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.14  
    2.15  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    2.16  val overwritelthy: theory -> (Rule.rls' * (string * Rule.rls)) list * (Rule.rls' * Rule.rls) list ->

     3.1 --- a/src/Tools/isac/CalcElements/contextC.sml	Thu Nov 14 12:00:13 2019 +0100
     3.2 +++ b/src/Tools/isac/CalcElements/contextC.sml	Thu Nov 14 12:08:05 2019 +0100
     3.3 @@ -14,9 +14,9 @@
     3.4    val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context
     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 transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
    3.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    3.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    3.12  end
    3.13  
    3.14  (* survey on handling contexts:

     4.1 --- a/src/Tools/isac/CalcElements/libraryC.sml	Thu Nov 14 12:00:13 2019 +0100
     4.2 +++ b/src/Tools/isac/CalcElements/libraryC.sml	Thu Nov 14 12:08:05 2019 +0100
     4.3 @@ -77,10 +77,10 @@
     4.4      val ~~~ : 'a list * 'b list -> ('a * 'b) list
     4.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     4.6      (* NONE *)
     4.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     4.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     4.9      val enumerate_strings: string list -> string list
    4.10      val quad2pair: 'a * 'b * 'c * 'd -> 'a * 'b
    4.11 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    4.12 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    4.13  
    4.14  
    4.15  (*///------------------------------>>> thy ------------------------------------------------\\\*)

     5.1 --- a/src/Tools/isac/CalcElements/rule.sml	Thu Nov 14 12:00:13 2019 +0100
     5.2 +++ b/src/Tools/isac/CalcElements/rule.sml	Thu Nov 14 12:08:05 2019 +0100
     5.3 @@ -110,11 +110,11 @@
     5.4      val terms2str': term list -> string                        (* shift up to Unparse *)
     5.5      val thm2str: thm -> string
     5.6      val thms2str : thm list -> string
     5.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     5.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     5.9      val string_of_thm': theory -> thm -> string                (* shift up to Unparse *)
    5.10      val string_of_thm: thm -> string                           (* shift up to Unparse *)
    5.11      val errpats2str : errpat list -> string
    5.12 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    5.13 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    5.14  
    5.15  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    5.16  

     6.1 --- a/src/Tools/isac/CalcElements/termC.sml	Thu Nov 14 12:00:13 2019 +0100
     6.2 +++ b/src/Tools/isac/CalcElements/termC.sml	Thu Nov 14 12:08:05 2019 +0100
     6.3 @@ -85,10 +85,10 @@
     6.4      val atomty_thy: Rule.thyID -> term -> unit
     6.5      val free2var: term -> term
     6.6      val contains_one_of: thm * (string * typ) list -> bool
     6.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     6.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     6.9      val atomt: term -> unit
    6.10      val typ_a2real: term -> term
    6.11 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    6.12 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    6.13    end
    6.14  
    6.15  (**)

     7.1 --- a/src/Tools/isac/Interpret/inform.sml	Thu Nov 14 12:00:13 2019 +0100
     7.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu Nov 14 12:08:05 2019 +0100
     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	Thu Nov 14 12:00:13 2019 +0100
     8.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Thu Nov 14 12:08:05 2019 +0100
     8.3 @@ -40,7 +40,7 @@
     8.4      | NasApp of Istate.pstate * Proof.context * Tactic.T
     8.5      | NasNap of  term * Env.T;
     8.6    val assoc2str : assoc -> string
     8.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     8.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     8.9    val go : Celem.path -> term -> term
    8.10    val go_up: Celem.path -> term -> term
    8.11    val check_Let_up : Istate.pstate -> term -> term * term
    8.12 @@ -57,7 +57,7 @@
    8.13    val scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> appy
    8.14    val go_scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> appy
    8.15    val scan_to_tactic2: term * (Ctree.state * Rule.theory') -> Istate.T -> appy
    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/rewtools.sml	Thu Nov 14 12:00:13 2019 +0100
     9.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Thu Nov 14 12:08:05 2019 +0100
     9.3 @@ -45,12 +45,12 @@
     9.4    val guh2theID : Celem.guh -> Celem.theID
     9.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     9.6    (*  NONE *)
     9.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     9.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     9.9    val trtas2str : (term * Rule.rule * (term * term list)) list -> string
    9.10    val eq_Thm : Rule.rule * Rule.rule -> bool
    9.11    val deriv2str : (term * Rule.rule * (term * term list)) list -> string
    9.12    val deriv_of_thm'' : Celem.thm'' -> string
    9.13 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    9.14 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    9.15  
    9.16  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    9.17    val deri2str : (Rule.rule * (term * term list)) list -> string

    10.1 --- a/src/Tools/isac/Interpret/script.sml	Thu Nov 14 12:00:13 2019 +0100
    10.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Nov 14 12:08:05 2019 +0100
    10.3 @@ -38,10 +38,10 @@
    10.4  
    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 is_spec_pos : Ctree.pos_ -> bool
   10.10    val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
   10.11 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   10.12 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   10.13  
   10.14  end 
   10.15  

    11.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml	Thu Nov 14 12:00:13 2019 +0100
    11.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml	Thu Nov 14 12:08:05 2019 +0100
    11.3 @@ -39,12 +39,12 @@
    11.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    11.5    val cappend_parent : CTbasic.ctree -> int list -> Istate.T * Proof.context -> term ->
    11.6      Tactic.input -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list
    11.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    11.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    11.9    val update_loc' : CTbasic.ctree -> CTbasic.pos ->
   11.10      (Istate.T * Proof.context) option * (Istate.T * Proof.context) option -> CTbasic.ctree
   11.11    val append_problem : int list -> Istate.T * Proof.context -> Selem.fmz ->
   11.12      Model.ori list * Celem.spec * term -> CTbasic.ctree -> CTbasic.ctree
   11.13 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   11.14 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   11.15  end
   11.16  (**)
   11.17  structure CTaccess(**): CALC_TREE_ACCESS(**) =

    12.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Thu Nov 14 12:00:13 2019 +0100
    12.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Thu Nov 14 12:08:05 2019 +0100
    12.3 @@ -106,7 +106,7 @@
    12.4    val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos   (* duplicate in ctree-navi.sml *)
    12.5     ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
    12.6  
    12.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    12.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    12.9    val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
   12.10    val pr_short : pos -> ppobj -> string
   12.11    val g_ctxt : ppobj -> Proof.context
   12.12 @@ -120,7 +120,7 @@
   12.13    val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
   12.14    val get_trace : ctree -> int list -> int list -> int list list
   12.15    val branch2str : branch -> string
   12.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   12.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   12.18  
   12.19  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   12.20    (* NONE *)

    13.1 --- a/src/Tools/isac/MathEngBasic/ctree-navi.sml	Thu Nov 14 12:00:13 2019 +0100
    13.2 +++ b/src/Tools/isac/MathEngBasic/ctree-navi.sml	Thu Nov 14 12:08:05 2019 +0100
    13.3 @@ -28,9 +28,9 @@
    13.4  
    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    (* NONE *)
   13.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   13.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   13.12  
   13.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   13.14    (* NONE *)

    14.1 --- a/src/Tools/isac/MathEngBasic/ctree.sml	Thu Nov 14 12:00:13 2019 +0100
    14.2 +++ b/src/Tools/isac/MathEngBasic/ctree.sml	Thu Nov 14 12:08:05 2019 +0100
    14.3 @@ -15,10 +15,10 @@
    14.4    open CTnavi
    14.5    open CTaccess
    14.6  end;
    14.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    14.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    14.9    open Ctree;
   14.10    open Pos
   14.11 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   14.12 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   14.13  
   14.14  (* policy for "open" structures:
   14.15  --------------------------------

    15.1 --- a/src/Tools/isac/MathEngBasic/model.sml	Thu Nov 14 12:00:13 2019 +0100
    15.2 +++ b/src/Tools/isac/MathEngBasic/model.sml	Thu Nov 14 12:08:05 2019 +0100
    15.3 @@ -51,9 +51,9 @@
    15.4    val penv2str_ : Proof.context -> penv -> string  (* NONE *)
    15.5    type preori
    15.6    val preoris2str : preori list -> string
    15.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    15.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    15.9    (* NONE *)
   15.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   15.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   15.12  
   15.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   15.14    val untouched : itm list -> bool

    16.1 --- a/src/Tools/isac/MathEngBasic/mstools.sml	Thu Nov 14 12:00:13 2019 +0100
    16.2 +++ b/src/Tools/isac/MathEngBasic/mstools.sml	Thu Nov 14 12:08:05 2019 +0100
    16.3 @@ -20,9 +20,9 @@
    16.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    16.5    val pres2str : (bool * term) list -> string
    16.6    val refined : match list -> Celem.pblID
    16.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    16.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    16.9    (*NONE*)
   16.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   16.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   16.12  
   16.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   16.14    val pblID_of_match : match -> Celem.pblID

    17.1 --- a/src/Tools/isac/MathEngBasic/position.sml	Thu Nov 14 12:00:13 2019 +0100
    17.2 +++ b/src/Tools/isac/MathEngBasic/position.sml	Thu Nov 14 12:08:05 2019 +0100
    17.3 @@ -21,8 +21,8 @@
    17.4  
    17.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    17.6    val pos's2str: pos' list -> string
    17.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    17.8 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    17.9 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   17.10 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   17.11  end
   17.12  
   17.13  (**)

    18.1 --- a/src/Tools/isac/MathEngBasic/specification-elems.sml	Thu Nov 14 12:00:13 2019 +0100
    18.2 +++ b/src/Tools/isac/MathEngBasic/specification-elems.sml	Thu Nov 14 12:08:05 2019 +0100
    18.3 @@ -33,9 +33,9 @@
    18.4    val e_sube : Rule.cterm' list
    18.5    val e_subs : string list
    18.6    val subte2subst : term list -> (term * term) list
    18.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    18.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    18.9    (*  NONE *)
   18.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   18.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   18.12  
   18.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   18.14  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)

    19.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Thu Nov 14 12:00:13 2019 +0100
    19.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Thu Nov 14 12:08:05 2019 +0100
    19.3 @@ -112,9 +112,9 @@
    19.4    val rule2tac : theory -> (term * term) list ->  Rule.rule -> input         (* for rewtools.sml *)
    19.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    19.6    (* NONE *)
    19.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    19.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    19.9    (* NONE *)
   19.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   19.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   19.12  
   19.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   19.14    (* NONE *)

    20.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml	Thu Nov 14 12:00:13 2019 +0100
    20.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml	Thu Nov 14 12:08:05 2019 +0100
    20.3 @@ -28,14 +28,14 @@
    20.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    20.5    val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Tactic.input) * Telem.safe * Ctree.ctree
    20.6    val f2str : Generate.mout -> Rule.cterm'
    20.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    20.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    20.9    type nxt_
   20.10    datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
   20.11    val loc_solve_ : string * Tactic.T -> Ctree.ctree *  Ctree.pos' -> lOc_
   20.12    val loc_specify_ : Tactic.T -> Ctree.state -> lOc_
   20.13    val nxt_specify_: Ctree.ctree * Ctree.pos' -> Chead.calcstate'
   20.14    val TESTg_form : Ctree.state -> Generate.mout
   20.15 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   20.16 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   20.17  
   20.18  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   20.19    (* NONE *)

    21.1 --- a/src/Tools/isac/MathEngine/solve.sml	Thu Nov 14 12:00:13 2019 +0100
    21.2 +++ b/src/Tools/isac/MathEngine/solve.sml	Thu Nov 14 12:08:05 2019 +0100
    21.3 @@ -23,9 +23,9 @@
    21.4    val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
    21.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    21.6    val get_form : tac'_ -> Ctree.pos' -> Ctree.ctree -> Generate.mout
    21.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    21.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    21.9    (*NONE*)
   21.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   21.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   21.12  
   21.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   21.14    (* NONE *)

    22.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Thu Nov 14 12:00:13 2019 +0100
    22.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Thu Nov 14 12:08:05 2019 +0100
    22.3 @@ -36,7 +36,7 @@
    22.4      val prep_rls: theory -> Rule.rls -> Rule.rls (*ren insert*)
    22.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    22.6    (* NONE *)
    22.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    22.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    22.9      val subst_typ: string -> typ -> term list -> (typ * typ) list
   22.10      val is_calc: term -> bool
   22.11      val rule2stac: theory -> Rule.rule -> term
   22.12 @@ -44,7 +44,7 @@
   22.13      val #> : term list -> term
   22.14      val rules2scr_Rls : theory -> Rule.rule list -> term
   22.15      val rules2scr_Seq : theory -> Rule.rule list -> term
   22.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   22.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   22.18    end
   22.19  (**)
   22.20  structure Auto_Prog(**): AUTO_GERNERATE_PROGRAM(**) =

    23.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy	Thu Nov 14 12:00:13 2019 +0100
    23.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy	Thu Nov 14 12:08:05 2019 +0100
    23.3 @@ -63,9 +63,9 @@
    23.4    val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * Celem.stacexpr
    23.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    23.6    (*NONE*)
    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  end 
   23.13  \<close> ML \<open>
   23.14  (**)

    24.1 --- a/src/Tools/isac/ProgLang/Program.thy	Thu Nov 14 12:00:13 2019 +0100
    24.2 +++ b/src/Tools/isac/ProgLang/Program.thy	Thu Nov 14 12:08:05 2019 +0100
    24.3 @@ -40,9 +40,9 @@
    24.4      val body_of : term -> term            (*ren body*)
    24.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    24.6    (* NONE *)
    24.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    24.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    24.9    (* NONE *)
   24.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   24.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   24.12    end
   24.13  \<close> ML \<open>
   24.14  \<close> ML \<open>

    25.1 --- a/src/Tools/isac/ProgLang/calculate.sml	Thu Nov 14 12:00:13 2019 +0100
    25.2 +++ b/src/Tools/isac/ProgLang/calculate.sml	Thu Nov 14 12:08:05 2019 +0100
    25.3 @@ -22,12 +22,12 @@
    25.4      val float_op_var: term -> string -> typ -> typ -> float -> term
    25.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    25.6    (* NONE *)
    25.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    25.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    25.9      val get_pair: theory -> string -> Rule.eval_fn -> term -> (string * term) option
   25.10      val mk_rule: term list * term * term -> term
   25.11      val divisors: int -> int list
   25.12      val doubles: int list -> int list
   25.13 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   25.14 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   25.15    end
   25.16  
   25.17  (**)

    26.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Thu Nov 14 12:00:13 2019 +0100
    26.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Thu Nov 14 12:08:05 2019 +0100
    26.3 @@ -23,7 +23,7 @@
    26.4        -> term -> (term * term list) option
    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      val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
   26.10        Rule.rls -> bool -> thm -> term -> (term * term list) option
   26.11      val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule.rls -> term -> (term * term list) option
   26.12 @@ -31,7 +31,7 @@
   26.13      val app_sub: theory -> int -> Rule.rls -> term -> term * term list * bool
   26.14      val mk_thm: theory -> string -> thm
   26.15      val trace1: int -> string -> unit
   26.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   26.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   26.18    end
   26.19  
   26.20  (**)

    27.1 --- a/src/Tools/isac/Specify/Input_Descript.thy	Thu Nov 14 12:00:13 2019 +0100
    27.2 +++ b/src/Tools/isac/Specify/Input_Descript.thy	Thu Nov 14 12:08:05 2019 +0100
    27.3 @@ -71,9 +71,9 @@
    27.4    val pbl_ids: Proof.context -> term -> term -> term list
    27.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    27.6    (* NONE *)
    27.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    27.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    27.9    (* NONE *)
   27.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   27.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   27.12  end
   27.13  \<close> ML \<open>
   27.14  (**)

    28.1 --- a/src/Tools/isac/Specify/appl.sml	Thu Nov 14 12:00:13 2019 +0100
    28.2 +++ b/src/Tools/isac/Specify/appl.sml	Thu Nov 14 12:08:05 2019 +0100
    28.3 @@ -10,9 +10,9 @@
    28.4    val applicable_in : Ctree.pos' -> Ctree.ctree -> Tactic.input -> Chead.appl
    28.5  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    28.6    val tac2tac_ : Ctree.ctree -> Ctree.pos' -> Tactic.input -> Tactic.T
    28.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    28.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    28.9    val mk_set : 'a -> ctree -> pos -> term -> term -> term * term list
   28.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   28.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   28.12  end
   28.13  
   28.14  (**)

    29.1 --- a/src/Tools/isac/Specify/calchead.sml	Thu Nov 14 12:00:13 2019 +0100
    29.2 +++ b/src/Tools/isac/Specify/calchead.sml	Thu Nov 14 12:08:05 2019 +0100
    29.3 @@ -106,7 +106,7 @@
    29.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    29.5    val e_calcstate : Ctree.state * Generate.taci list
    29.6    val e_calcstate' : calcstate'
    29.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    29.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    29.9    val posterms2str : (pos' * term * 'a) list -> string
   29.10    val postermtacs2str : (pos' * term * Tactic.input option) list -> string
   29.11    val vals_of_oris : Model.ori list -> term list
   29.12 @@ -124,7 +124,7 @@
   29.13      Model.itm list -> (string * (term * term)) list -> Rule.cterm' -> additm
   29.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
   29.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
   29.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   29.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   29.18  
   29.19  (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
   29.20    val variants_in : term list -> int

    30.1 --- a/src/Tools/isac/Specify/generate.sml	Thu Nov 14 12:00:13 2019 +0100
    30.2 +++ b/src/Tools/isac/Specify/generate.sml	Thu Nov 14 12:08:05 2019 +0100
    30.3 @@ -31,9 +31,9 @@
    30.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    30.5    val tacis2str : taci list -> string
    30.6    val mout2str : mout -> string
    30.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    30.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    30.9    (*  NONE *)
   30.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   30.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   30.12  
   30.13  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   30.14    (* NONE *)

    31.1 --- a/src/Tools/isac/Specify/ptyps.sml	Thu Nov 14 12:00:13 2019 +0100
    31.2 +++ b/src/Tools/isac/Specify/ptyps.sml	Thu Nov 14 12:08:05 2019 +0100
    31.3 @@ -55,7 +55,7 @@
    31.4    val e_errpat : Rule.errpat
    31.5    val show_pblguhs : unit -> unit
    31.6    val sort_pblguhs : unit -> unit
    31.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    31.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    31.9    val add_field : theory -> Celem.pat list -> term * 'b -> string * term * 'b
   31.10    val add_variants : ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
   31.11    val coll_variants: ('a * ''b) list -> ('a list * ''b) list
   31.12 @@ -63,7 +63,7 @@
   31.13    val max: int list -> int
   31.14    val replace_0: int -> int list -> int list
   31.15    val split_did: term -> term * term
   31.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   31.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   31.18  
   31.19  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
   31.20    val e_fillpat : string * term * string