author | haftmann |
Mon, 05 Jun 2017 21:24:39 +0200 | |
changeset 66022 | cc8e9289a6c4 |
parent 66021 | 08ab52fb9db5 |
child 66023 | 22ef720a92b0 |
--- 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