Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Function/lexicographic_order.ML
changeset 82590 d08f5b5ead0a
parent 82300 838f29a19f48 
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Apr 25 16:54:39 2025 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Apr 25 18:06:12 2025 +0200
@@ -124,16 +124,12 @@
 
 fun pr_unprovable_cell _ ((i,j), Less _) = []
   | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
-      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
-       Goal_Display.string_of_goal ctxt st]
+      [Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <):") st]
   | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
-      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
-       Goal_Display.string_of_goal ctxt st_less ^
-       "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^
-       Goal_Display.string_of_goal ctxt st_leq]
+      [Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <):") st_less ^ "\n" ^
+       Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):") st_leq]
   | pr_unprovable_cell ctxt ((i,j), False st) =
-      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
-       Goal_Display.string_of_goal ctxt st]
+      [Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <):") st]
 
 fun pr_unprovable_subgoals ctxt table =
   table
isabelle