src/Tools/isac/MathEngBasic/tactic.sml
changeset 59778 148d369e6b71
parent 59773 d88bb023c380
child 59784 9800556c5cfe
     1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon Jan 20 11:11:56 2020 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Mon Jan 20 11:48:59 2020 +0100
     1.3 @@ -102,9 +102,10 @@
     1.4    | Tac of string
     1.5    | Take of Rule.cterm' | Take_Inst of Rule.cterm'
     1.6    val tac2str : input -> string
     1.7 +  val is_empty_tac : input -> bool
     1.8  
     1.9 +(*//-------------------------------------------------------------- only AFTER ctree.sml required *)
    1.10    val eq_tac : input * input -> bool
    1.11 -  val is_empty_tac : input -> bool
    1.12    val is_rewtac : input -> bool
    1.13    val is_rewset : input -> bool
    1.14    val rls_of : input -> Rule.rls'