src/HOL/ROOT
changeset 51115 7dbd6832a689
parent 51093 9d7aa2bb097b
child 51143 0a2371e7ced3
--- a/src/HOL/ROOT	Thu Feb 14 12:24:56 2013 +0100
+++ b/src/HOL/ROOT	Thu Feb 14 14:14:55 2013 +0100
@@ -26,6 +26,8 @@
     Finite_Lattice
     Code_Char_chr
     Code_Char_ord
+    Product_Lexorder
+    Product_Order
     Code_Integer
     Efficient_Nat
     (* Code_Prolog  FIXME cf. 76965c356d2a *)