1.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy	Tue Nov 19 16:18:16 2019 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy	Thu Nov 21 12:05:56 2019 +0100
     1.3 @@ -48,19 +48,19 @@
     1.4    Take         :: "'a => 'a"
     1.5  
     1.6    (* legacy.. *)
     1.7 -  Calculate1   :: "[char list, 'a] => 'a" (* unknown to lucas-interpreter *)
     1.8    Check'_elementwise :: (* TODO: is idle, retained for test purposes in Minisubpbl *)
     1.9  		  "['a list, 'b set] => 'a list" ("Check'_elementwise (_ _)" 11)
    1.10    Assumptions  :: bool  (* TODO: remove with making ^^^ idle *)
    1.11  
    1.12  
    1.13 -subsection \<open>TODO\<close>
    1.14 +subsection \<open>ML code for Prog_Tac\<close>
    1.15  ML \<open>
    1.16  signature PROGAM_TACTIC =
    1.17  sig
    1.18    val dest_spec : term -> Celem.spec
    1.19    val get_stac : 'a -> term -> term option (*rename get_first*)
    1.20    val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * Celem.stacexpr
    1.21 +  val is: term -> bool
    1.22  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.23    (*NONE*)
    1.24  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.25 @@ -180,6 +180,25 @@
    1.26    | subst_stacexpr E a v t = 
    1.27      (a, Celem.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t));
    1.28  
    1.29 +
    1.30 +(* check if a term is a Prog_Tac *)
    1.31 +
    1.32 +val SOME Calculate = TermC.parseNEW @{context} "Calculate";
    1.33 +val SOME Rewrite = TermC.parseNEW @{context} "Rewrite";
    1.34 +val SOME Rewrite_Inst = TermC.parseNEW @{context} "Rewrite'_Inst";
    1.35 +val SOME Rewrite_Set = TermC.parseNEW @{context} "Rewrite'_Set";
    1.36 +val SOME Rewrite_Set_Inst = TermC.parseNEW @{context} "Rewrite'_Set'_Inst";
    1.37 +val SOME Or_to_List = TermC.parseNEW @{context} "Or'_to'_List";
    1.38 +val SOME SubProblem = TermC.parseNEW @{context} "SubProblem";
    1.39 +val SOME Substitute = TermC.parseNEW @{context} "Substitute";
    1.40 +val SOME Take = TermC.parseNEW @{context} "Take";
    1.41 +val SOME Check_elementwise = TermC.parseNEW @{context} "Check'_elementwise";
    1.42 +val SOME Assumptions = TermC.parseNEW @{context} "Assumptions";
    1.43 +
    1.44 +val all_Consts = [Calculate, Rewrite, Rewrite_Inst, Rewrite_Set, Rewrite_Set_Inst, Or_to_List,
    1.45 +  SubProblem, Substitute, Take, Check_elementwise, Assumptions]
    1.46 +
    1.47 +fun is t = TermC.contains_Const_typeless all_Consts t
    1.48  (**)end(**)
    1.49  \<close> ML \<open>
    1.50  \<close>