src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Wed Dec 08 18:18:36 2010 +0100
+++ b/src/FOL/FOL.thy	Wed Feb 23 11:23:26 2011 +0100
@@ -11,6 +11,7 @@
   "~~/src/Provers/blast.ML"
   "~~/src/Provers/clasimp.ML"
   "~~/src/Tools/induct.ML"
+  "~~/src/Tools/case_product.ML"
   ("cladata.ML")
   ("simpdata.ML")
 begin
@@ -391,6 +392,8 @@
 setup Induct.setup
 declare case_split [cases type: o]
 
+setup Case_Product.setup
+
 
 hide_const (open) eq