tuned;
authorwenzelm
Sat Dec 19 15:20:38 2015 +0100 (2015-12-19)
changeset 618666fa60a4f7e48
parent 61865 6dcc9e4f1aa6
child 61867 95cce5313c83
tuned;
src/Doc/Isar_Ref/Proof_Script.thy
     1.1 --- a/src/Doc/Isar_Ref/Proof_Script.thy	Sat Dec 19 15:14:59 2015 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy	Sat Dec 19 15:20:38 2015 +0100
     1.3 @@ -102,8 +102,8 @@
     1.4    apply} sequences.
     1.5  
     1.6    The current goal state, which is essentially a hidden part of the Isar/VM
     1.7 -  configurtation, is turned into a proof context and remaining conclusion.
     1.8 -  This correponds to @{command fix}~/ @{command assume}~/ @{command show} in
     1.9 +  configuration, is turned into a proof context and remaining conclusion.
    1.10 +  This corresponds to @{command fix}~/ @{command assume}~/ @{command show} in
    1.11    structured proofs, but the text of the parameters, premises and conclusion
    1.12    is not given explicitly.
    1.13