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