changeset 7353 | b5a5abea1559 |
parent 7332 | 60534b9018ae |
child 7417 | 70c1d3eac214 |
--- a/src/Pure/Isar/isar_thy.ML Wed Aug 25 20:39:18 1999 +0200 +++ b/src/Pure/Isar/isar_thy.ML Wed Aug 25 20:39:50 1999 +0200 @@ -339,7 +339,7 @@ Pretty.block [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Proof.pretty_thm thm]; fun pretty_rule thm = - Pretty.block [Pretty.str "solving goal by rule:", Pretty.fbrk, Proof.pretty_thm thm]; + Pretty.block [Pretty.str "trying to solve goal by rule:", Pretty.fbrk, Proof.pretty_thm thm]; val print_result = Pretty.writeln o pretty_result;