diff options
Diffstat (limited to 'theories/Bool/Sumbool.v')
| -rw-r--r-- | theories/Bool/Sumbool.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 0da72f56..06ab77cf 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Sumbool.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) (** Here are collected some results about the type sumbool (see INIT/Specif.v) [sumbool A B], which is written [{A}+{B}], is the informative @@ -39,18 +39,18 @@ Defined. Section connectives. Variables A B C D : Prop. - + Hypothesis H1 : {A} + {B}. Hypothesis H2 : {C} + {D}. - + Definition sumbool_and : {A /\ C} + {B \/ D}. case H1; case H2; auto. Defined. - + Definition sumbool_or : {A \/ C} + {B /\ D}. case H1; case H2; auto. Defined. - + Definition sumbool_not : {B} + {A}. case H1; auto. Defined. |