--- a/ProgTutorial/Base.thy	Tue May 14 13:39:31 2019 +0200
+++ b/ProgTutorial/Base.thy	Tue May 14 16:59:53 2019 +0200
@@ -3,17 +3,12 @@
         "~~/src/HOL/Library/LaTeXsugar"
 begin
 
-ML \<open>@{assert} true\<close>
-ML \<open>@{print} (2 + 3 +4)\<close>
-
+print_ML_antiquotations
 
-print_ML_antiquotations
-text \<open>
-Can we put an ML-val into the text?
+text \<open>Hallo ML Antiquotation:
+@{ML \<open>2 + 3\<close>}
+\<close>
 
-@{ML [display] \<open>2 + 3\<close>}
-
-\<close>
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 
@@ -30,17 +25,16 @@
   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 *}*) (* Seems to be standard now, we don't need this anymoe *)
 setup {* AntiquoteSetup.setup *}
 
+print_ML_antiquotations
+
+text \<open>Hallo ML Antiquotation:
+@{ML \<open>2 + 3\<close> }
+\<close>
 
 end
\ No newline at end of file