diff options
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/ClassicalDescription.v | 2 | ||||
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 4 | ||||
| -rw-r--r-- | theories/Logic/ConstructiveEpsilon.v | 4 | ||||
| -rw-r--r-- | theories/Logic/Diaconescu.v | 2 |
4 files changed, 5 insertions, 7 deletions
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index aa65eb44c..855588602 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -21,7 +21,7 @@ Set Implicit Arguments. Require Export Classical. Require Import ChoiceFacts. -Notation Local "'inhabited' A" := A (at level 200, only parsing). +Notation Local inhabited A := A. Axiom constructive_definite_description : forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }. diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index f3f177a73..6673fa8c9 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -119,7 +119,7 @@ Qed. *) -Definition inhabited (A:Prop) := A. +Notation Local inhabited A := A. Lemma prop_ext_A_eq_A_imp_A : prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A. @@ -514,8 +514,6 @@ Qed. 344 of Lecture Notes in Mathematics, Springer-Verlag, 1973. *) -Notation Local "'inhabited' A" := A (at level 10, only parsing). - Definition IndependenceOfGeneralPremises := forall (A:Type) (P:A -> Prop) (Q:Prop), inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x. diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index fe571779c..83d5e002a 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id:$ i*) +(*i $Id$ i*) (** This module proves the constructive description schema, which infers the sigma-existence (i.e., [Set]-existence) of a witness to a @@ -53,7 +53,7 @@ of our searching algorithm. *) Let R (x y : nat) : Prop := x = S y /\ ~ P y. -Notation Local "'acc' x" := (Acc R x) (at level 10). +Notation Local acc x := (Acc R x). Lemma P_implies_acc : forall x : nat, P x -> acc x. Proof. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index a954cbef7..b96ae30e4 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -267,7 +267,7 @@ End ProofIrrel_RelChoice_imp_EqEM. (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) -Notation Local "'inhabited' A" := A (at level 10, only parsing). +Notation Local inhabited A := A. Section ExtensionalEpsilon_imp_EM. |