diff options
| -rw-r--r-- | theories/Init/Notations.v | 4 | ||||
| -rw-r--r-- | theories/Logic/Diaconescu.v | 10 |
2 files changed, 7 insertions, 7 deletions
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 1ab6219f06..845837e480 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -8,9 +8,9 @@ (*i $Id$ i*) -(** These are the notations whose level and associativity is imposed by Coq *) +(** These are the notations whose level and associativity are imposed by Coq *) -(** Notations for logical connectives *) +(** Notations for propositional connectives *) Reserved Notation "x <-> y" (at level 95, no associativity). Reserved Notation "x /\ y" (at level 80, right associativity). diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 73a2f3e9b7..d815b9dda7 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -97,23 +97,23 @@ Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P. Proof. intro P. -(* first we exhibit the choice functional relation R *) +(** first we exhibit the choice functional relation R *) destruct AC as [R H]. set (class_of_true := fun b => b = true \/ P). set (class_of_false := fun b => b = false \/ P). -(* the actual "decision": is (R class_of_true) = true or false? *) +(** the actual "decision": is (R class_of_true) = true or false? *) destruct (H class_of_true) as [b0 [H0 [H0' H0'']]]. exists true; left; reflexivity. destruct H0. -(* the actual "decision": is (R class_of_false) = true or false? *) +(** the actual "decision": is (R class_of_false) = true or false? *) destruct (H class_of_false) as [b1 [H1 [H1' H1'']]]. exists false; left; reflexivity. destruct H1. -(* case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *) +(** case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *) right. intro HP. assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b). @@ -129,7 +129,7 @@ rewrite <- H0''. reflexivity. rewrite Heq. assumption. -(* cases where P is true *) +(** cases where P is true *) left; assumption. left; assumption. |