# HG changeset patch # User paulson # Date 1065177376 -7200 # Node ID 9fdea25f9ebb6d7805710ca134d275866802a1e5 # Parent db95d1c2f51b33107a48c026eeba70afeac35e0e added a comment diff -r db95d1c2f51b -r 9fdea25f9ebb TFL/tfl.ML --- a/TFL/tfl.ML Thu Oct 02 10:57:04 2003 +0200 +++ b/TFL/tfl.ML Fri Oct 03 12:36:16 2003 +0200 @@ -446,6 +446,9 @@ val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats val (case_rewrites,context_congs) = extraction_thms theory + (*case_ss causes minimal simplification: bodies of case expressions are + not simplified. Otherwise large examples (Red-Black trees) are too + slow.*) val case_ss = HOL_basic_ss addcongs DatatypePackage.weak_case_congs_of theory addsimps case_rewrites val corollaries' = map (Simplifier.simplify case_ss) corollaries