diff -r 6103b0eadbf2 -r f7c97e64cc2a ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Base.thy	Thu May 16 19:56:12 2019 +0200
@@ -5,10 +5,10 @@
 
 print_ML_antiquotations
 
-text \<open>Hallo ML Antiquotation:
-@{ML \<open>2 + 3\<close>}
+text \<open>
+Why is Base not printed?
+@{cite "isa-imp"}
 \<close>
-
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 
@@ -33,8 +33,4 @@
 
 print_ML_antiquotations
 
-text \<open>Hallo ML Antiquotation:
-@{ML \<open>2 + 3\<close> }
-\<close>
-
 end
\ No newline at end of file