changeset 54398 | 100c0eaf63d5 |
parent 49834 | b27bbb021df1 |
child 55415 | 05f5fdb8d093 |
--- a/src/HOL/Datatype.thy Tue Nov 12 13:47:24 2013 +0100 +++ b/src/HOL/Datatype.thy Tue Nov 12 13:47:24 2013 +0100 @@ -499,7 +499,7 @@ (*Dependent version*) lemma dprod_subset_Sigma2: - "(dprod (Sigma A B) (Sigma C D)) <= + "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))" by auto @@ -522,4 +522,3 @@ setup Datatype_Realizer.setup end -