2 files changed, 14 insertions, 35 deletions

diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v
index 8a88642f3..0b0c329be 100755
--- a/theories/Logic/Classical_Pred_Set.v
+++ b/theories/Logic/Classical_Pred_Set.v
@@ -8,9 +8,12 @@
 
 (*i $Id$ i*)
 
+(** This file is obsolete, use Classical_Pred_Type.v via Classical.v
+instead *)
+
 (** Classical Predicate Logic on Set*)
 
-Require Import Classical_Prop.
+Require Import Classical_Pred_Type.
 
 Section Generic.
 Variable U : Set.
@@ -19,52 +22,26 @@ Variable U : Set.
 
 Lemma not_all_ex_not :
  forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U, ~ P n.
-Proof.
-unfold not in |- *; intros P notall.
-apply NNPP; unfold not in |- *.
-intro abs.
-cut (forall n:U, P n); auto.
-intro n; apply NNPP.
-unfold not in |- *; intros.
-apply abs; exists n; trivial.
-Qed.
+Proof (Classical_Pred_Type.not_all_ex_not U).
 
 Lemma not_all_not_ex :
  forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U, P n.
-Proof.
-intros P H.
-elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n.
-apply NNPP; trivial.
-Qed.
+Proof (Classical_Pred_Type.not_all_not_ex U).
 
 Lemma not_ex_all_not :
  forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
-Proof.
-unfold not in |- *; intros P notex n abs.
-apply notex.
-exists n; trivial.
-Qed. 
+Proof (Classical_Pred_Type.not_ex_all_not U).
 
 Lemma not_ex_not_all :
  forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n.
-Proof.
-intros P H n.
-apply NNPP.
-red in |- *; intro K; apply H; exists n; trivial.
-Qed.
+Proof (Classical_Pred_Type.not_ex_not_all U).
 
 Lemma ex_not_not_all :
  forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).
-Proof.
-unfold not in |- *; intros P exnot allP.
-elim exnot; auto.
-Qed.
+Proof (Classical_Pred_Type.ex_not_not_all U).
 
 Lemma all_not_not_ex :
  forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n).
-Proof.
-unfold not in |- *; intros P allnot exP; elim exP; intros n p.
-apply allnot with n; auto.
-Qed.
+Proof (Classical_Pred_Type.all_not_not_ex U).
 
-End Generic.
\ No newline at end of file
+End Generic.
diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v
index fc5d162a2..3b91afd02 100755
--- a/theories/Logic/Classical_Type.v
+++ b/theories/Logic/Classical_Type.v
@@ -8,7 +8,9 @@
 
 (*i $Id$ i*)
 
+(** This file is obsolete, use Classical.v instead *)
+
 (** Classical Logic for Type *)
 
 Require Export Classical_Prop.
-Require Export Classical_Pred_Type.
\ No newline at end of file
+Require Export Classical_Pred_Type.