1 files changed, 0 insertions, 77 deletions
diff --git a/theories7/Bool/Sumbool.v b/theories7/Bool/Sumbool.v
deleted file mode 100644
index 8d55cbb6..00000000
--- a/theories7/Bool/Sumbool.v
+++ /dev/null
@@ -1,77 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: Sumbool.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ 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
-   disjunction "A or B", where A and B are logical propositions.
-   Its extraction is isomorphic to the type of booleans. *)
-
-(** A boolean is either [true] or [false], and this is decidable *)
-
-Definition sumbool_of_bool : (b:bool) {b=true}+{b=false}.
-Proof.
-  NewDestruct b; Auto.
-Defined.
-
-Hints Resolve sumbool_of_bool : bool.
-
-Definition bool_eq_rec : (b:bool)(P:bool->Set)
-                    ((b=true)->(P true))->((b=false)->(P false))->(P b).
-NewDestruct b; Auto.
-Defined.
-
-Definition bool_eq_ind : (b:bool)(P:bool->Prop)
-                    ((b=true)->(P true))->((b=false)->(P false))->(P b).
-NewDestruct b; Auto.
-Defined.
-
-
-(*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno i*)
-
-(** Logic connectives on type [sumbool] *)
-
-Section connectives.
-
-Variables A,B,C,D : Prop.
-
-Hypothesis H1 : {A}+{B}.
-Hypothesis H2 : {C}+{D}.
-
-Definition sumbool_and : {A/\C}+{B\/D}.
-Proof.
-Case H1; Case H2; Auto.
-Defined.
-
-Definition sumbool_or : {A\/C}+{B/\D}.
-Proof.
-Case H1; Case H2; Auto.
-Defined.
-
-Definition sumbool_not : {B}+{A}.
-Proof.
-Case H1; Auto.
-Defined.
-
-End connectives.
-
-Hints Resolve sumbool_and sumbool_or sumbool_not : core.
-
-
-(** Any decidability function in type [sumbool] can be turned into a function
-    returning a boolean with the corresponding specification: *)
-
-Definition bool_of_sumbool : 
-  (A,B:Prop) {A}+{B} -> { b:bool | if b then A else B }.
-Proof.
-Intros A B H.
-Elim H; [ Intro; Exists true; Assumption
-        | Intro; Exists false; Assumption ].
-Defined.
-Implicits bool_of_sumbool.