author | paulson |
Thu, 28 Dec 1995 11:54:15 +0100 | |
changeset 1423 | 5726a8243d3f |
parent 1422 | bc628f4ef0cb |
child 1424 | ccb3c5ff6707 |
src/HOL/Sum.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Sum.thy Sat Dec 23 12:50:53 1995 +0100 +++ b/src/HOL/Sum.thy Thu Dec 28 11:54:15 1995 +0100 @@ -41,7 +41,7 @@ Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))" Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))" sum_case_def "sum_case f g p == @z. (!x. p=Inl(x) --> z=f(x)) - & (!y. p=Inr(y) --> z=g(y))" + & (!y. p=Inr(y) --> z=g(y))" sum_def "A plus B == (Inl``A) Un (Inr``B)"