diff -r 97d6d0a72d35 -r b9cf6801f3da 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.
 *};