src/HOL/Library/ROOT.ML
author wenzelm
Tue Aug 03 16:57:45 2010 +0200 (2010-08-03)
changeset 38137 6fda94059baa
parent 38119 src/HOL/Library/HOL_Library_ROOT.ML@e00f970425e9
child 38504 76965c356d2a
permissions -rw-r--r--
renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
haftmann@37694
     1
haftmann@37694
     2
(* Classical Higher-order Logic -- batteries included *)
haftmann@37694
     3
haftmann@37694
     4
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
bulwahn@38119
     5
  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];