src/HOL/Multivariate_Analysis/ROOT.ML
changeset 33267 8fb01a2f9406
parent 33175 2083bde13ce1
child 33615 261abc2e3155
equal deleted inserted replaced
33266:2172ae12c81d 33267:8fb01a2f9406
     1 (*
       
     2   no_document use_thy "ThisTheory";
       
     3   use_thy "ThatTheory";
       
     4 *)
       
     5 
       
     6 use_thy "Multivariate_Analysis";
     1 use_thy "Multivariate_Analysis";