doc-src/IsarAdvanced/Functions/Thy/ROOT.ML
changeset 21212 547224bf9348
equal deleted inserted replaced
21211:5370cfbf3070 21212:547224bf9348
       
     1 
       
     2 (* $Id$ *)
       
     3 
       
     4 use_thy "Functions";