Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified signature: do not expose internal operation;
authorwenzelm
Tue, 28 Aug 2018 10:58:43 +0200
changeset 68825 8207c67d9ef4
parent 68824 7414ce0256e1
child 68826 deefe5837120
clarified signature: do not expose internal operation;
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy file | annotate | diff | comparison | revisions
src/Pure/tactic.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Mon Aug 27 22:58:36 2018 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Aug 28 10:58:43 2018 +0200
@@ -1490,7 +1490,7 @@
 ML \<open>
 fun remove_duplicates_tac feats =
   (if can_feature (CleanUp [RemoveDuplicates]) feats then
-     ALLGOALS distinct_subgoal_tac
+     distinct_subgoals_tac
    else all_tac)
 \<close>
 
--- a/src/Pure/tactic.ML	Mon Aug 27 22:58:36 2018 +0200
+++ b/src/Pure/tactic.ML	Tue Aug 28 10:58:43 2018 +0200
@@ -28,7 +28,6 @@
   val ematch_tac: Proof.context -> thm list -> int -> tactic
   val dmatch_tac: Proof.context -> thm list -> int -> tactic
   val flexflex_tac: Proof.context -> tactic
-  val distinct_subgoal_tac: int -> tactic
   val distinct_subgoals_tac: tactic
   val cut_tac: thm -> int -> tactic
   val cut_rules_tac: thm list -> int -> tactic
isabelle