ProgTutorial/First_Steps.thy
changeset 575 c3dbc04471a9
parent 572 438703674711
--- a/ProgTutorial/First_Steps.thy	Wed May 22 12:38:51 2019 +0200
+++ b/ProgTutorial/First_Steps.thy	Wed May 22 13:24:30 2019 +0200
@@ -880,9 +880,9 @@
 setup %gray \<open>term_pat_setup\<close>
 
 text \<open>
-  The parser in Line 2 provides us with a context and a string; this string is
+  The parser in Line 3 provides us with a context and a string; this string is
   transformed into a term using the function @{ML_ind read_term_pattern in
-  Proof_Context} (Line 5); the next two lines transform the term into a string
+  Proof_Context} (Line 6); the next two lines transform the term into a string
   so that the ML-system can understand it. (All these functions will be explained
   in more detail in later sections.) An example for this antiquotation is: