changeset 13784 | b9f6154427a4 |
parent 13615 | 449a70d88b38 |
child 13823 | d49ffd9f9662 |
--- a/src/ZF/QPair.thy Thu Jan 23 09:16:53 2003 +0100 +++ b/src/ZF/QPair.thy Thu Jan 23 10:30:14 2003 +0100 @@ -283,7 +283,7 @@ !!x. x: A ==> c(x): C(QInl(x)); !!y. y: B ==> d(y): C(QInr(y)) |] ==> qcase(c,d,u) : C(u)" -by (simp add: qsum_defs , auto) +by (simp add: qsum_defs, auto) (** Rules for the Part primitive **)