src/HOL/Library/ROOT.ML
changeset 47108 2a1953f0d20d
parent 45985 2d399a776de2
child 47232 e2f0176149d0
     1.1 --- a/src/HOL/Library/ROOT.ML	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Library/ROOT.ML	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -4,4 +4,4 @@
     1.4  use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order",
     1.5    "Product_Lattice",
     1.6    "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat"(*, "Code_Prolog"*),
     1.7 -  "Code_Real_Approx_By_Float" ];
     1.8 +  "Code_Real_Approx_By_Float", "Target_Numeral"];