src/HOL/Import/Generate-HOL/ROOT.ML
changeset 41589 bbd861837ebc
parent 15647 b1f486a9c56b
child 44367 74c08021ab2e
equal deleted inserted replaced
41588:9546828c0eb3 41589:bbd861837ebc
     1 (*  Title:      HOL/Import/Generate-HOL/ROOT.ML
       
     2     ID:         $Id$
       
     3     Author:     Sebastian Skalberg (TU Muenchen)
       
     4 *)
       
     5 
       
     6 use_thy "GenHOL4Prob";
     1 use_thy "GenHOL4Prob";
     7 use_thy "GenHOL4Vec";
     2 use_thy "GenHOL4Vec";
     8 use_thy "GenHOL4Word32";
     3 use_thy "GenHOL4Word32";