1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Thu Dec 19 12:40:17 2019 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Thu Dec 19 16:41:57 2019 +0100
     1.3 @@ -114,6 +114,8 @@
     1.4    val result : T -> term
     1.5    val creates_assms: T -> term list
     1.6    val insert_assumptions: T -> Proof.context -> Proof.context
     1.7 +  val for_specify: input -> bool
     1.8 +  val for_specify': T -> bool
     1.9  
    1.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.11    (* NONE *)
    1.12 @@ -504,4 +506,33 @@
    1.13  
    1.14  fun insert_assumptions tac ctxt  = ContextC.insert_assumptions (creates_assms tac) ctxt
    1.15  
    1.16 +fun for_specify (Init_Proof _) = true
    1.17 +  | for_specify Model_Problem  = true
    1.18 +  | for_specify (Refine_Tacitly _) = true
    1.19 +  | for_specify (Refine_Problem _) = true
    1.20 +  | for_specify (Add_Given _) = true
    1.21 +  | for_specify (Del_Given _) = true
    1.22 +  | for_specify (Add_Find _) = true
    1.23 +  | for_specify (Del_Find _) = true
    1.24 +  | for_specify (Add_Relation _) = true
    1.25 +  | for_specify (Del_Relation _) = true
    1.26 +  | for_specify (Specify_Theory _) = true
    1.27 +  | for_specify (Specify_Problem _) = true
    1.28 +  | for_specify (Specify_Method _) = true
    1.29 +  | for_specify _ = false
    1.30 +fun for_specify' (Init_Proof' _) = true
    1.31 +  | for_specify' (Model_Problem' _) = true
    1.32 +  | for_specify' (Refine_Tacitly' _) = true
    1.33 +  | for_specify' (Refine_Problem' _) = true
    1.34 +  | for_specify' (Add_Given' _) = true
    1.35 +  | for_specify' (Del_Given' _) = true
    1.36 +  | for_specify' (Add_Find' _) = true
    1.37 +  | for_specify' (Del_Find' _) = true
    1.38 +  | for_specify' (Add_Relation' _) = true
    1.39 +  | for_specify' (Del_Relation' _) = true
    1.40 +  | for_specify' (Specify_Theory' _) = true
    1.41 +  | for_specify' (Specify_Problem' _) = true
    1.42 +  | for_specify' (Specify_Method' _) = true
    1.43 +  | for_specify' _ = false
    1.44 +
    1.45  (**)end(**)