doc-src/IsarRef/Thy/ROOT-ZF.ML
changeset 42651 e3fdb7c96be5
parent 38767 d8da44a8dd25
equal deleted inserted replaced
42650:552eae49f97d 42651:e3fdb7c96be5
     1 Thy_Output.source_default := true;
     1 quick_and_dirty := true;
     2 use "../../antiquote_setup.ML";
       
     3 
     2 
     4 use_thy "ZF_Specific";
     3 use_thy "ZF_Specific";