1.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml	Fri Dec 20 09:57:45 2019 +0100
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml	Fri Dec 20 10:24:52 2019 +0100
     1.3 @@ -190,8 +190,8 @@
     1.4  (*\\******************* locatetac returns tac_ + istate + cstate *****************************//*)
     1.5  
     1.6  "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
     1.7 -      val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
     1.8 -      (*if*) member op = Solve.specsteps mI; (*else*)
     1.9 +      val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
    1.10 +      (*if*) Tactic.for_specify' m; (*false*)
    1.11  
    1.12          (*val Updated (cs' as (_, _, (_, p'))) =*) loc_solve_ m ptp;
    1.13  "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp); 

     2.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Fri Dec 20 09:57:45 2019 +0100
     2.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Fri Dec 20 10:24:52 2019 +0100
     2.3 @@ -36,8 +36,8 @@
     2.4  
     2.5  "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
     2.6  "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
     2.7 -val Appl m = applicable_in p pt m;
     2.8 -member op = specsteps mI (*false*);
     2.9 +val Appl m = applicable_in p pt tac;
    2.10 + (*if*) Tactic.for_specify' m; (*false*)
    2.11  "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
    2.12  
    2.13  "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
    2.14 @@ -108,8 +108,8 @@
    2.15  
    2.16      (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **)  (*case*) locatetac tac (pt,p) (*of*);
    2.17  "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
    2.18 -      val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
    2.19 -      (*if*) member op = Solve.specsteps mI; (*else*)
    2.20 +      val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
    2.21 +      (*if*) Tactic.for_specify' m; (*false*)
    2.22  
    2.23        (** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ m ptp;
    2.24  "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
    2.25 @@ -271,8 +271,8 @@
    2.26  (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
    2.27  (** )val ("ok", (_, _, ptp as (pt, p))) =( **) locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
    2.28  "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (hd (sel_appl_atomic_tacs pt p), (pt, p));
    2.29 -      val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
    2.30 -      (*if*) member op = Solve.specsteps mI (*else*);
    2.31 +      val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
    2.32 +      (*if*) Tactic.for_specify' m; (*false*)
    2.33  
    2.34        loc_solve_ m ptp;
    2.35  "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);

     3.1 --- a/test/Tools/isac/Interpret/script.sml	Fri Dec 20 09:57:45 2019 +0100
     3.2 +++ b/test/Tools/isac/Interpret/script.sml	Fri Dec 20 10:24:52 2019 +0100
     3.3 @@ -59,8 +59,8 @@
     3.4  
     3.5  (*locatetac tac (pt, ip); (*WAS scan_dn1: call by ([3], Pbl)*)*)
     3.6  "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
     3.7 -applicable_in p pt m ; (*Appl*)
     3.8 -member op = specsteps mI; (*false*)
     3.9 +  val Appl m = applicable_in p pt tac ; (*Appl*)
    3.10 +  (*if*) Tactic.for_specify' m; (*false*)
    3.11  (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
    3.12  loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
    3.13  (*val it = fn: string * tac_ -> ctree * (pos * pos_) -> lOc_*)
    3.14 @@ -107,8 +107,8 @@
    3.15  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.16  "~~~~~ fun me, args:"; val tac = nxt;
    3.17  "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
    3.18 -val Appl m = applicable_in p pt m;
    3.19 -member op = specsteps mI; (*false*)
    3.20 +val Appl m = applicable_in p pt tac;
    3.21 + (*if*) Tactic.for_specify' m; (*false*)
    3.22  "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
    3.23  "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))
    3.24    = (m, pos);

     4.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Fri Dec 20 09:57:45 2019 +0100
     4.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Fri Dec 20 10:24:52 2019 +0100
     4.3 @@ -184,7 +184,7 @@
     4.4  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
     4.5  "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
     4.6  "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
     4.7 -val Appl m = applicable_in p pt m;
     4.8 +val Appl m = applicable_in p pt tac;
     4.9  val Check_elementwise' (trm1, str, (trm2, trms)) = m;
    4.10  term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
    4.11  str = "Assumptions";
    4.12 @@ -196,7 +196,7 @@
    4.13    "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n     (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n     0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^
    4.14    "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n     (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n     0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]";
    4.15  (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
    4.16 -member op = specsteps mI (*false*);
    4.17 +      (*if*) Tactic.for_specify' m; (*false*)
    4.18  (*loc_solve_ (mI,m) ptp;
    4.19    WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
    4.20  "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);

     5.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Fri Dec 20 09:57:45 2019 +0100
     5.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Fri Dec 20 10:24:52 2019 +0100
     5.3 @@ -47,8 +47,8 @@
     5.4  "~~~~~ fun me, args:"; val tac = nxt;
     5.5  val ("ok", (_, _, (pt''''',p'''''))) = locatetac tac (pt,p);
     5.6  "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
     5.7 -val Appl m = applicable_in p pt m; (*m = Apply_Method'..*)
     5.8 -member op = specsteps mI; (*false*)
     5.9 +val Appl m = applicable_in p pt tac; (*m = Apply_Method'..*)
    5.10 + (*if*) Tactic.for_specify' m; (*false*)
    5.11  "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);
    5.12  "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,_), pos as (p,_)) = (m, pos);
    5.13  val PblObj {meth, ctxt, ...} = get_obj I pt p;

     6.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Fri Dec 20 09:57:45 2019 +0100
     6.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Fri Dec 20 10:24:52 2019 +0100
     6.3 @@ -35,8 +35,8 @@
     6.4  (*ERROR WAS: scan_dn1: call by ([3], Pbl)*)
     6.5  val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt,p) (*of*);
     6.6  "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
     6.7 -val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
     6.8 -member op = Solve.specsteps mI (* = false*);
     6.9 +val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
    6.10 +  (*if*) Tactic.for_specify' m; (*false*)
    6.11  
    6.12             loc_solve_ m ptp ;  (* scan_dn1: call by ([3], Pbl)*)
    6.13  "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos)) = (m, ptp);

     7.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Fri Dec 20 09:57:45 2019 +0100
     7.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Fri Dec 20 10:24:52 2019 +0100
     7.3 @@ -26,8 +26,8 @@
     7.4  "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
     7.5  
     7.6  "~~~~~ fun locatetac , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
     7.7 -val Appl m = applicable_in p pt m;
     7.8 -member op = specsteps mI; (*false*)
     7.9 +  val Appl m = applicable_in p pt tac;
    7.10 +  (*if*) Tactic.for_specify' m; (*false*)
    7.11  (*val Updated (cs' as (_,_,(_,p'))) =  loc_solve_ (mI,m) ptp;*)
    7.12  "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
    7.13  (*val (msg, cs') =*)

     8.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Fri Dec 20 09:57:45 2019 +0100
     8.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Fri Dec 20 10:24:52 2019 +0100
     8.3 @@ -40,8 +40,8 @@
     8.4  
     8.5         locatetac tac (pt, p) (*of*);
     8.6  "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
     8.7 -   val Appl m = (*case*) applicable_in p pt m (*of*);
     8.8 -   member op = specsteps mI; (*else*)
     8.9 +   val Appl m = (*case*) applicable_in p pt tac (*of*);
    8.10 +  (*if*) Tactic.for_specify' m; (*false*)
    8.11  
    8.12             loc_solve_ m ptp;
    8.13  "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);

     9.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Fri Dec 20 09:57:45 2019 +0100
     9.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Fri Dec 20 10:24:52 2019 +0100
     9.3 @@ -168,7 +168,7 @@
     9.4    ML_file "ProgLang/prog_expr.sml"
     9.5    ML_file "ProgLang/program.sml"
     9.6    ML_file "ProgLang/prog_tac.sml"
     9.7 -  ML_file "ProgLang/tactical.sml"
     9.8 +  ML_file "ProgLang/tactical.sml"                 
     9.9    ML_file "ProgLang/auto_prog.sml"
    9.10    ML_file "ProgLang/rewrite.sml"
    9.11    ML_file "ProgLang/tools.sml"