# HG changeset patch
# User Simon Wimmer <wimmers@in.tum.de>
# Date 1710189991 -3600
# Node ID d3811cf07da6c1dedb0eb86cc96bec59fea0c7d0
# Parent  0d5c41ea208ab9032c16f5d9f08dc1b7efd7ffa6
sketch & explore: TODO comments are addressed in parent commits

diff -r 0d5c41ea208a -r d3811cf07da6 src/HOL/ex/Sketch_and_Explore.thy
--- a/src/HOL/ex/Sketch_and_Explore.thy	Mon Mar 11 21:11:23 2024 +0100
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Mon Mar 11 21:46:31 2024 +0100
@@ -26,7 +26,6 @@
   t
   |> singleton (Syntax.uncheck_terms ctxt)
   |> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt
-      \<comment> \<open>TODO pointless to annotate explicit fixes in term\<close>
   |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
   |> Sledgehammer_Util.simplify_spaces
   |> ATP_Util.maybe_quote ctxt;
@@ -41,7 +40,6 @@
   let
     val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt;
     val prefix = replicate_string indent " ";
-      \<comment> \<open>TODO consider pre-existing indentation -- how?\<close>
     val prefix_sep = "\n" ^ prefix ^ "    and ";
     val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl;
     val if_s = if null assms then NONE