doc-src/TutorialI/Types/Setup.thy
changeset 43564 9864182c6bad
parent 31678 752f23a37240
child 48891 c0eafbd55de3
equal deleted inserted replaced
43563:aeabb735883a 43564:9864182c6bad
     3 uses
     3 uses
     4   "../../antiquote_setup.ML"
     4   "../../antiquote_setup.ML"
     5   "../../more_antiquote.ML"
     5   "../../more_antiquote.ML"
     6 begin
     6 begin
     7 
     7 
       
     8 setup {* Antiquote_Setup.setup #> More_Antiquote.setup *}
       
     9 
       
    10 
     8 end
    11 end