clarified message
authorhaftmann
Mon, 05 Jun 2017 21:24:39 +0200
changeset 66022 cc8e9289a6c4
parent 66021 08ab52fb9db5
child 66023 22ef720a92b0
clarified message
src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jun 06 13:42:38 2017 +0200
+++ b/src/Pure/Isar/code.ML	Mon Jun 05 21:24:39 2017 +0200
@@ -883,7 +883,7 @@
       end;
 
 fun pretty_cert thy (cert as Nothing _) =
-      [Pretty.str "(not implemented)"]
+      [Pretty.str "(no equations)"]
   | pretty_cert thy (cert as Equations _) =
       (map_filter
         (Option.map (Thm.pretty_thm_global thy o