src/HOL/Library/ROOT.ML
changeset 38137 6fda94059baa
parent 38119 e00f970425e9
child 38504 76965c356d2a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/ROOT.ML	Tue Aug 03 16:57:45 2010 +0200
     1.3 @@ -0,0 +1,5 @@
     1.4 +
     1.5 +(* Classical Higher-order Logic -- batteries included *)
     1.6 +
     1.7 +use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
     1.8 +  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];