src/HOL/Product_Type.thy
changeset 14337 e13731554e50
parent 14208 144f45277d5a
child 14359 3d9948163018
--- a/src/HOL/Product_Type.thy	Sat Jan 03 16:09:39 2004 +0100
+++ b/src/HOL/Product_Type.thy	Mon Jan 05 00:46:06 2004 +0100
@@ -484,7 +484,11 @@
   apply (rule ext, blast)
   done
 
-lemma split_comp_eq [simp]: 
+(* Do NOT make this a simp rule as it
+   a) only helps in special situations
+   b) can lead to nontermination in the presence of split_def
+*)
+lemma split_comp_eq: 
 "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
 by (rule ext, auto)