src/HOL/Multivariate_Analysis/ROOT.ML
changeset 33175 2083bde13ce1
child 33267 8fb01a2f9406
equal deleted inserted replaced
33083:1fad3160d873 33175:2083bde13ce1
       
     1 (*
       
     2   no_document use_thy "ThisTheory";
       
     3   use_thy "ThatTheory";
       
     4 *)
       
     5 
       
     6 use_thy "Multivariate_Analysis";