1.1 --- a/src/HOL/Library/HOL_Library_ROOT.ML	Fri Jul 02 14:23:17 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,1 +0,0 @@
     1.4 -use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"];

     2.1 --- a/src/HOL/ROOT.ML	Fri Jul 02 14:23:17 2010 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Fri Jul 02 14:23:17 2010 +0200
     2.3 @@ -1,3 +1,4 @@
     2.4 -(* Classical Higher-order Logic -- batteries included *)
     2.5 +
     2.6 +(* Classical Higher-order Logic *)
     2.7  
     2.8  use_thys ["Complex_Main"];

     3.1 --- a/src/HOL/base.ML	Fri Jul 02 14:23:17 2010 +0200
     3.2 +++ b/src/HOL/base.ML	Fri Jul 02 14:23:17 2010 +0200
     3.3 @@ -1,2 +1,4 @@
     3.4 -(*side-entry for HOL-Base*)
     3.5 +
     3.6 +(* side-entry for HOL-Base *)
     3.7 +
     3.8  use_thys ["HOL"];

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/library.ML	Fri Jul 02 14:23:17 2010 +0200
     4.3 @@ -0,0 +1,5 @@
     4.4 +
     4.5 +(* Classical Higher-order Logic -- batteries included *)
     4.6 +
     4.7 +use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
     4.8 +  "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"];

     5.1 --- a/src/HOL/main.ML	Fri Jul 02 14:23:17 2010 +0200
     5.2 +++ b/src/HOL/main.ML	Fri Jul 02 14:23:17 2010 +0200
     5.3 @@ -1,2 +1,4 @@
     5.4 -(*side-entry for HOL-Main*)
     5.5 +
     5.6 +(* side-entry for HOL-Main *)
     5.7 +
     5.8  use_thys ["Main"];

     6.1 --- a/src/HOL/plain.ML	Fri Jul 02 14:23:17 2010 +0200
     6.2 +++ b/src/HOL/plain.ML	Fri Jul 02 14:23:17 2010 +0200
     6.3 @@ -1,2 +1,4 @@
     6.4 -(*side-entry for HOL-Plain*)
     6.5 +
     6.6 +(* side-entry for HOL-Plain *)
     6.7 +
     6.8  use_thys ["Plain"];