doc-src/IsarRef/Thy/Base.thy
changeset 48891 c0eafbd55de3
parent 43564 9864182c6bad
child 48956 d54a3d39ba85
equal deleted inserted replaced
48890:d72ca5742f80 48891:c0eafbd55de3
     1 theory Base
     1 theory Base
     2 imports Pure
     2 imports Pure
     3 uses "../../antiquote_setup.ML"
       
     4 begin
     3 begin
       
     4 
       
     5 ML_file "../../antiquote_setup.ML"
     5 
     6 
     6 setup {*
     7 setup {*
     7   Antiquote_Setup.setup #>
     8   Antiquote_Setup.setup #>
     8   member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup
     9   member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup
     9 *}
    10 *}