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 *}