src/HOL/HOL.thy
changeset 41827 98eda7ffde79
parent 41792 ff3cb0c418b7
child 41865 4e8483cc2cc5
--- a/src/HOL/HOL.thy	Wed Dec 08 18:18:36 2010 +0100
+++ b/src/HOL/HOL.thy	Wed Feb 23 11:23:26 2011 +0100
@@ -31,10 +31,12 @@
   ("Tools/recfun_codegen.ML")
   ("Tools/cnf_funcs.ML")
   "~~/src/Tools/subtyping.ML"
+  "~~/src/Tools/case_product.ML"
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
 setup Subtyping.setup
+setup Case_Product.setup
 
 
 subsection {* Primitive logic *}