src/HOL/Isar_examples/BasicLogic.thy

--- a/src/HOL/Isar_examples/BasicLogic.thy	Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Sat Aug 19 12:44:39 2000 +0200
@@ -221,7 +221,7 @@
 qed;
 
 text {*
- We can still push forward reasoning a bit further, even at the risk
+ We can still push forward-reasoning a bit further, even at the risk
  of getting ridiculous.  Note that we force the initial proof step to
  do nothing here, by referring to the ``-'' proof method.
 *};