src/ZF/Sum.thy
 changeset 13356 c9cfe1638bf2 parent 13255 407ad9c3036d child 13823 d49ffd9f9662
```     1.1 --- a/src/ZF/Sum.thy	Sun Jul 14 15:11:21 2002 +0200
1.2 +++ b/src/ZF/Sum.thy	Sun Jul 14 15:14:43 2002 +0200
1.3 @@ -3,12 +3,14 @@
1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.5      Copyright   1993  University of Cambridge
1.6
1.7 -Disjoint sums in Zermelo-Fraenkel Set Theory
1.8 -"Part" primitive for simultaneous recursive type definitions
1.9  *)
1.10
1.12 +
1.13  theory Sum = Bool + equalities:
1.14
1.15 +text{*And the "Part" primitive for simultaneous recursive type definitions*}
1.16 +
1.17  global
1.18
1.19  constdefs
1.20 @@ -30,7 +32,7 @@
1.21
1.22  local
1.23
1.24 -(*** Rules for the Part primitive ***)
1.25 +subsection{*Rules for the @{term Part} Primitive*}
1.26
1.27  lemma Part_iff:
1.28      "a : Part(A,h) <-> a:A & (EX y. a=h(y))"
1.29 @@ -56,7 +58,7 @@
1.30  done
1.31
1.32
1.33 -(*** Rules for Disjoint Sums ***)
1.34 +subsection{*Rules for Disjoint Sums*}
1.35
1.36  lemmas sum_defs = sum_def Inl_def Inr_def case_def
1.37
1.38 @@ -130,7 +132,7 @@
1.39  by (simp add: sum_def, blast)
1.40
1.41
1.42 -(*** Eliminator -- case ***)
1.43 +subsection{*The Eliminator: @{term case}*}
1.44
1.45  lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)"