src/HOL/Isar_examples/Peirce.thy
 changeset 7982 d534b897ce39 parent 7874 180364256231 child 10007 64bf7da1994a
     1.1 --- a/src/HOL/Isar_examples/Peirce.thy	Sat Oct 30 20:13:16 1999 +0200
1.2 +++ b/src/HOL/Isar_examples/Peirce.thy	Sat Oct 30 20:20:48 1999 +0200
1.3 @@ -75,15 +75,15 @@
1.4   individual parts of the proof configuration.
1.5
1.6   Nevertheless, the strong'' mode of plain assumptions is quite
1.7 - important in practice to achieve robustness of proof document
1.8 + important in practice to achieve robustness of proof text
1.9   interpretation.  By forcing both the conclusion \emph{and} the
1.10   assumptions to unify with the pending goal to be solved, goal
1.11   selection becomes quite deterministic.  For example, decomposition
1.12 - with case-analysis'' type rules usually give rise to several goals
1.13 - that only differ in there local contexts.  With strong assumptions
1.14 - these may be still solved in any order in a predictable way, while
1.15 - weak ones would quickly lead to great confusion, eventually demanding
1.16 - even some backtracking.
1.17 + with rules of the case-analysis'' type usually gives rise to
1.18 + several goals that only differ in there local contexts.  With strong
1.19 + assumptions these may be still solved in any order in a predictable
1.20 + way, while weak ones would quickly lead to great confusion,
1.21 + eventually demanding even some backtracking.
1.22  *};
1.23
1.24  end;