--- a/src/Doc/Isar_Ref/Proof_Script.thy Sat Dec 19 15:14:59 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Sat Dec 19 15:20:38 2015 +0100
@@ -102,8 +102,8 @@
apply} sequences.
The current goal state, which is essentially a hidden part of the Isar/VM
- configurtation, is turned into a proof context and remaining conclusion.
- This correponds to @{command fix}~/ @{command assume}~/ @{command show} in
+ configuration, is turned into a proof context and remaining conclusion.
+ This corresponds to @{command fix}~/ @{command assume}~/ @{command show} in
structured proofs, but the text of the parameters, premises and conclusion
is not given explicitly.