doc-src/IsarRef/Thy/Base.thy
changeset 43564 9864182c6bad
parent 42651 e3fdb7c96be5
child 48891 c0eafbd55de3
equal deleted inserted replaced
43563:aeabb735883a 43564:9864182c6bad
     2 imports Pure
     2 imports Pure
     3 uses "../../antiquote_setup.ML"
     3 uses "../../antiquote_setup.ML"
     4 begin
     4 begin
     5 
     5 
     6 setup {*
     6 setup {*
       
     7   Antiquote_Setup.setup #>
     7   member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup
     8   member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup
     8 *}
     9 *}
     9 
    10 
    10 declare [[thy_output_source]]
    11 declare [[thy_output_source]]
    11 
    12