src/HOL/ROOT.ML
changeset 2019 b45d9f2042e0
parent 1982 38aafcab6890
child 2115 9709f9188549
     1.1 --- a/src/HOL/ROOT.ML	Tue Sep 24 08:59:24 1996 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Tue Sep 24 09:02:34 1996 +0200
     1.3 @@ -38,6 +38,7 @@
     1.4  use_thy "RelPow";
     1.5  use_thy "Finite";
     1.6  use_thy "Sexp";
     1.7 +use_thy "Option";
     1.8  use_thy "List";
     1.9  
    1.10  init_pps ();