# HG changeset patch
# User wenzelm
# Date 1450534838 -3600
# Node ID 6fa60a4f7e487a2268b243e6713d2629389c70b7
# Parent  6dcc9e4f1aa65315080a4c07ee8efcda4e814460
tuned;

diff -r 6dcc9e4f1aa6 -r 6fa60a4f7e48 src/Doc/Isar_Ref/Proof_Script.thy
--- 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.