| changeset 44006 | b9839fad3bb6 |
| parent 42841 | 9079f49053e5 |
| child 44561 | 73f84bf0c6ac |
--- a/src/HOL/Library/ROOT.ML Sun Jul 31 11:13:38 2011 -0700 +++ b/src/HOL/Library/ROOT.ML Mon Aug 01 09:31:10 2011 -0700 @@ -2,4 +2,5 @@ (* Classical Higher-order Logic -- batteries included *) use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order", + "Product_Lattice", "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];