clarified signature: do not expose internal operation;
authorwenzelm
Tue Aug 28 10:58:43 2018 +0200 (13 months ago)
changeset 688258207c67d9ef4
parent 68824 7414ce0256e1
child 68826 deefe5837120
clarified signature: do not expose internal operation;
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
src/Pure/tactic.ML
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Mon Aug 27 22:58:36 2018 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Aug 28 10:58:43 2018 +0200
     1.3 @@ -1490,7 +1490,7 @@
     1.4  ML \<open>
     1.5  fun remove_duplicates_tac feats =
     1.6    (if can_feature (CleanUp [RemoveDuplicates]) feats then
     1.7 -     ALLGOALS distinct_subgoal_tac
     1.8 +     distinct_subgoals_tac
     1.9     else all_tac)
    1.10  \<close>
    1.11  
     2.1 --- a/src/Pure/tactic.ML	Mon Aug 27 22:58:36 2018 +0200
     2.2 +++ b/src/Pure/tactic.ML	Tue Aug 28 10:58:43 2018 +0200
     2.3 @@ -28,7 +28,6 @@
     2.4    val ematch_tac: Proof.context -> thm list -> int -> tactic
     2.5    val dmatch_tac: Proof.context -> thm list -> int -> tactic
     2.6    val flexflex_tac: Proof.context -> tactic
     2.7 -  val distinct_subgoal_tac: int -> tactic
     2.8    val distinct_subgoals_tac: tactic
     2.9    val cut_tac: thm -> int -> tactic
    2.10    val cut_rules_tac: thm list -> int -> tactic