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;