--- a/ProgTutorial/Base.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Base.thy	Tue May 14 11:10:53 2019 +0200
@@ -3,11 +3,21 @@
         "~~/src/HOL/Library/LaTeXsugar"
 begin
 
+ML \<open>@{assert} true\<close>
+ML \<open>@{print} (2 + 3 +4)\<close>
+
+
+print_ML_antiquotations
+text \<open>
+Can we put an ML-val into the text?
+
+@{ML [display] \<open>2 + 3\<close>}
+
+\<close>
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 
-ML {*
-fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
+ML %linenosgrayML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
 
 fun rhs 1 = P 1
   | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
@@ -17,13 +27,20 @@
                  (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
 
 fun de_bruijn n =
-  HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
-*}
+  HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
 
 ML_file "output_tutorial.ML"
+text \<open>
+Can we put an ML-val into the text?
+
+@{ML [gray] \<open>2 + 3\<close>}
+\<close>
+
 ML_file "antiquote_setup.ML"
 
-setup {* OutputTutorial.setup *}
+
+(*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *)
 setup {* AntiquoteSetup.setup *}
 
+
 end
\ No newline at end of file