src/Doc/Tutorial/Inductive/Advanced.thy
changeset 72991 d0a0b74f0ad7
parent 69605 a96320074298
--- a/src/Doc/Tutorial/Inductive/Advanced.thy	Wed Dec 23 22:25:22 2020 +0100
+++ b/src/Doc/Tutorial/Inductive/Advanced.thy	Wed Dec 23 23:03:03 2020 +0100
@@ -1,6 +1,4 @@
-(*<*)theory Advanced imports Even begin
-ML_file \<open>../../antiquote_setup.ML\<close>
-(*>*)
+(*<*)theory Advanced imports Even begin(*>*)
 
 text \<open>
 The premises of introduction rules may contain universal quantifiers and