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