# HG changeset patch
# User wenzelm
# Date 1424804271 -3600
# Node ID 3ff1dd7ac7f090ba44fb171d82d1b05ee99841e1
# Parent  d28b3b79fba837321433020ffec0fbd3e9251a75
tuned;

diff -r d28b3b79fba8 -r 3ff1dd7ac7f0 src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Tue Feb 24 08:48:09 2015 +0100
+++ b/src/Doc/Implementation/Proof.thy	Tue Feb 24 19:57:51 2015 +0100
@@ -437,9 +437,9 @@
   it.  The latter may depend on the local assumptions being presented
   as facts.  The result is in HHF normal form.
 
-  \item @{ML Goal.prove_common}~@{text "ctxt fork_pri"} is the general form
+  \item @{ML Goal.prove_common}~@{text "ctxt fork_pri"} is the common form
   to state and prove a simultaneous goal statement, where @{ML Goal.prove}
-  is a convenient shorthand for the most common application.
+  is a convenient shorthand that is most frequently used in applications.
 
   The given list of simultaneous conclusions is encoded in the goal state by
   means of Pure conjunction: @{ML Goal.conjunction_tac} will turn this into