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