diff -r 95b42288294e -r 438703674711 ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/First_Steps.thy	Tue May 21 14:37:39 2019 +0200
@@ -4,7 +4,6 @@
                                                   
 chapter \<open>First Steps\label{chp:firststeps}\<close>
 
-
 text \<open>
   \begin{flushright}
   {\em ``The most effective debugging tool is still careful thought,\\ 
@@ -109,10 +108,9 @@
   You can print out error messages with the function @{ML_ind error in Library}; 
   for example:
 
-  @{ML_matchresult_fake [display,gray] 
+  @{ML_response [display,gray] 
   \<open>if 0 = 1 then true else (error "foo")\<close> 
-\<open>*** foo
-***\<close>}
+\<open>foo\<close>}
 
   This function raises the exception \<open>ERROR\<close>, which will then 
   be displayed by the infrastructure indicating that it is an error by
@@ -132,11 +130,14 @@
 
 ML %grayML\<open>val pretty_term = Syntax.pretty_term
 val pwriteln = Pretty.writeln\<close>
-
+(* We redfine pwriteln to return a value not just a side effect on the output in order to
+use some checking of output with ML_response antiquotation. *)
+ML %invisible\<open>val pretty_term = Syntax.pretty_term
+val pwriteln = YXML.content_of o Pretty.string_of\<close>
 text \<open>
   They can be used as follows
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>pwriteln (pretty_term @{context} @{term "1::nat"})\<close>
   \<open>"1"\<close>}
 
@@ -159,7 +160,7 @@
 text \<open>
   Now by using this context @{ML pretty_term} prints out
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>pwriteln (pretty_term show_types_ctxt @{term "(1::nat, x)"})\<close>
   \<open>(1::nat, x::'a)\<close>}
 
@@ -203,7 +204,7 @@
   @{thm [source] conjI} shown below can be used for any (typable) 
   instantiation of \<open>?P\<close> and \<open>?Q\<close>. 
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>pwriteln (pretty_thm @{context} @{thm conjI})\<close>
   \<open>\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\<close>}
 
@@ -221,7 +222,7 @@
 text \<open>
   With this function, theorem @{thm [source] conjI} is now printed as follows:
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>pwriteln (pretty_thm_no_vars @{context} @{thm conjI})\<close>
   \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q\<close>}
   
@@ -267,12 +268,12 @@
 @{ML_matchresult_fake [display,gray]
 \<open>pwriteln (Pretty.str "First half,"); 
 pwriteln (Pretty.str "and second half.")\<close>
-\<open>First half,
-and second half.\<close>}
+\<open>"First half,
+and second half."\<close>}
 
   but as a single string with appropriate formatting. For example
 
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
 \<open>pwriteln (Pretty.str ("First half," ^ "\\n" ^ "and second half."))\<close>
 \<open>First half,
 and second half.\<close>}
@@ -282,7 +283,7 @@
   @{ML_ind cat_lines in Library} concatenates a list of strings 
   and inserts newlines in between each element. 
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>pwriteln (Pretty.str (cat_lines ["foo", "bar"]))\<close>
   \<open>foo
 bar\<close>}
@@ -387,7 +388,7 @@
   applied to it. For example, below three variables are applied to the term 
   @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
 \<open>let
   val trm = @{term "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}
   val ctxt = @{context}
@@ -414,7 +415,7 @@
   terms involving fresh variables. For this the infrastructure helps
   tremendously to avoid any name clashes. Consider for example:
 
-   @{ML_matchresult_fake [display,gray]
+   @{ML_response [display,gray]
 \<open>let
   val trm = @{term "za::'a \<Rightarrow> 'b \<Rightarrow> 'c"}
   val ctxt = @{context}
@@ -599,7 +600,7 @@
 
   An example where this combinator is useful is as follows
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_matchresult [display, gray]
   \<open>let
   val ((names1, names2), _) =
     @{context}
@@ -639,12 +640,12 @@
   both as pairs. We can use this information for example to print out the definiens and 
   the theorem corresponding to the definitions. For example for the first definition:
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>let 
   val (one_trm, (_, one_thm)) = one_def
 in
-  pwriteln (pretty_term ctxt' one_trm);
-  pwriteln (pretty_thm ctxt' one_thm)
+  (pwriteln (pretty_term ctxt' one_trm),
+   pwriteln (pretty_thm ctxt' one_thm))
 end\<close>
   \<open>One
 One \<equiv> 1\<close>}
@@ -673,7 +674,7 @@
   @{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check 
   a list of terms. Consider the code:
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
   \<open>let
   val ctxt = @{context}
 in
@@ -694,7 +695,7 @@
   Syntax} in the file @{ML_file "Pure/Syntax/syntax.ML"} that is implemented 
   in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example
 
-  @{ML_matchresult_fake [display, gray, linenos]
+  @{ML_response [display, gray, linenos]
   \<open>let 
   val ctxt = @{context}
 in
@@ -774,7 +775,7 @@
   @{ML_matchresult_fake [display, gray]
   \<open>Proof_Context.print_abbrevs false @{context}\<close>
 \<open>\<dots>
-INTER \<equiv> INFI
+INTER \<equiv> INFIMUM
 Inter \<equiv> Inf
 \<dots>\<close>}
 
@@ -783,21 +784,22 @@
   You can also use antiquotations to refer to proved theorems: 
   \<open>@{thm \<dots>}\<close> for a single theorem
 
-  @{ML_matchresult_fake [display,gray] \<open>@{thm allI}\<close> \<open>(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x\<close>}
+  @{ML_response [display,gray] \<open>@{thm allI}\<close> \<open>(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x\<close>}
 
   and \<open>@{thms \<dots>}\<close> for more than one
 
-@{ML_matchresult_fake [display,gray] 
+
+@{ML_response [display,gray] 
   \<open>@{thms conj_ac}\<close> 
-\<open>(?P \<and> ?Q) = (?Q \<and> ?P)
-(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
-((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)\<close>}  
+\<open>["(?P \<and> ?Q) = (?Q \<and> ?P)", 
+  "(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)", 
+  "((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"]\<close>}  
 
   The thm-antiquotations can also be used for manipulating theorems. For 
   example, if you need the version of the theorem @{thm [source] refl} that 
   has a meta-equality instead of an equality, you can write
 
-@{ML_matchresult_fake [display,gray] 
+@{ML_response [display,gray] 
   \<open>@{thm refl[THEN eq_reflection]}\<close>
   \<open>?x \<equiv> ?x\<close>}
 
@@ -816,7 +818,7 @@
 text \<open>
   The result can be printed out as follows.
 
-  @{ML_matchresult_fake [gray,display]
+  @{ML_response [gray,display]
 \<open>foo_thms |> pretty_thms_no_vars @{context}
          |> pwriteln\<close>
   \<open>True, False \<Longrightarrow> P\<close>}
@@ -840,9 +842,9 @@
   simp-rules. Now you can feed in the current simpset into this function. 
   The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.
 
-  @{ML_matchresult_fake [display,gray] 
+  @{ML_response [display,gray] 
   \<open>get_thm_names_from_ss @{context}\<close> 
-  \<open>["Nat.of_nat_eq_id", "Int.of_int_eq_id", "Nat.One_nat_def", \<dots>]\<close>}
+  \<open>["Euclidean_Division.euclidean_size_int_def",\<dots>\<close>}
 
   Again, this way of referencing simpsets makes you independent from additions
   of lemmas to the simpset by the user, which can potentially cause loops in your
@@ -884,9 +886,9 @@
   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:
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_matchresult [display,gray]
   \<open>@{term_pat "Suc (?x::nat)"}\<close>
-  \<open>Const ("Suc", "nat \<Rightarrow> nat") $ Var (("x", 0), "nat")\<close>}
+  \<open>Const ("Nat.Suc", _) $ Var (("x", 0), _)\<close>}
 
   which shows the internal representation of the term \<open>Suc ?x\<close>. Similarly
   we can write an antiquotation for type patterns. Its code is
@@ -980,19 +982,19 @@
 text \<open>
   The data can be retrieved with the projection functions defined above.
   
-  @{ML_matchresult_fake [display, gray]
-\<open>project_int (nth foo_list 0); 
-project_bool (nth foo_list 1)\<close> 
-\<open>13
+  @{ML_response [display, gray]
+\<open>(project_int (nth foo_list 0), 
+project_bool (nth foo_list 1))\<close> 
+\<open>13,
 true\<close>}
 
   Notice that we access the integer as an integer and the boolean as
   a boolean. If we attempt to access the integer as a boolean, then we get 
   a runtime error. 
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
 \<open>project_bool (nth foo_list 0)\<close>  
-\<open>*** exception Match raised\<close>}
+\<open>exception Match raised\<close>}
 
   This runtime error is the reason why ML is still type-sound despite
   containing a universal type.
@@ -1062,7 +1064,7 @@
   \emph{current} theory is updated (this is explained further in 
   Section~\ref{sec:theories}). The lookup can now be performed as follows.
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
 \<open>lookup @{theory} "conj"\<close>
 \<open>SOME "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"\<close>}
 
@@ -1073,10 +1075,11 @@
 
 setup %gray \<open>update "conj" @{thm TrueI}\<close>
 
+
 text \<open>
   and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}
   
-@{ML_matchresult_fake [display, gray]
+@{ML_response [display, gray]
 \<open>lookup @{theory} "conj"\<close>
 \<open>SOME "True"\<close>}
 
@@ -1271,9 +1274,9 @@
   The rules in the list can be retrieved using the function 
   @{ML FooRules.get}:
 
-  @{ML_matchresult_fake [display,gray] 
+  @{ML_response [display,gray] 
   \<open>FooRules.get @{context}\<close> 
-  \<open>["True", "?C","?B"]\<close>}
+  \<open>["True", "?C", "?B"]\<close>}
 
   Note that this function takes a proof context as argument. This might be 
   confusing, since the theorem list is stored as theory data. It becomes clear by knowing