tuned;
authorwenzelm
Sat, 19 Dec 2015 15:20:38 +0100
changeset 61868 6fa60a4f7e48
parent 61867 6dcc9e4f1aa6
child 61869 95cce5313c83
tuned;
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.