From 04a0a522a9a69e3cf1368110207af095a5860e7e Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 12 Oct 2000 16:25:29 +0000 Subject: Parentheses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@703 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sets/Powerset.v | 8 +++---- theories/Sets/Powerset_facts.v | 4 ++-- theories/Sets/Relations_2_facts.v | 2 +- theories/Sets/Relations_3_facts.v | 48 +++++++++++++++++++-------------------- 4 files changed, 31 insertions(+), 31 deletions(-) (limited to 'theories/Sets') diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index 0db6c1012..9b2f57809 100755 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -146,8 +146,8 @@ Theorem Union_is_Lub: Intros A a b H' H'0. Apply Lub_definition; Simpl. Apply Upper_Bound_definition; Simpl; Auto with sets. -(Intros y H'1; Elim H'1); Auto with sets. -(Intros y H'1; Elim H'1); Simpl; Auto with sets. +Intros y H'1; Elim H'1; Auto with sets. +Intros y H'1; Elim H'1; Simpl; Auto with sets. Qed. Theorem Intersection_is_Glb: @@ -162,8 +162,8 @@ Apply Glb_definition; Simpl. Apply Lower_Bound_definition; Simpl; Auto with sets. Apply Definition_of_Power_set. Generalize Inclusion_is_transitive; Intro IT; Red in IT; Apply IT with a; Auto with sets. -(Intros y H'1; Elim H'1); Auto with sets. -(Intros y H'1; Elim H'1); Simpl; Auto with sets. +Intros y H'1; Elim H'1; Auto with sets. +Intros y H'1; Elim H'1; Simpl; Auto with sets. Qed. End The_power_set_partial_order. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index b886f1211..57e51123d 100755 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -81,7 +81,7 @@ Theorem Couple_as_union: (x, y: U) (Union U (Singleton U x) (Singleton U y)) == (Couple U x y). Proof. Intros x y; Apply Extensionality_Ensembles; Split; Red. -Intros x0 H'; Elim H'; (Intros x1 H'0; Elim H'0; Auto with sets). +Intros x0 H'; Elim H'; '(Intros x1 H'0; Elim H'0; Auto with sets). Intros x0 H'; Elim H'; Auto with sets. Qed. @@ -92,7 +92,7 @@ Theorem Triple_as_union : Proof. Intros x y z; Apply Extensionality_Ensembles; Split; Red. Intros x0 H'; Elim H'. -Intros x1 H'0; Elim H'0; (Intros x2 H'1; Elim H'1; Auto with sets). +Intros x1 H'0; Elim H'0; '(Intros x2 H'1; Elim H'1; Auto with sets). Intros x1 H'0; Elim H'0; Auto with sets. Intros x0 H'; Elim H'; Auto with sets. Qed. diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index d5854165a..05f3753be 100755 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -38,7 +38,7 @@ Qed. Theorem Rstar_contains_R : (U: Type) (R: (Relation U)) (contains U (Rstar U R) R). Proof. -(Intros U R; Red); Intros x y H'; Apply Rstar_n with y; Auto with sets. +Intros U R; Red; Intros x y H'; Apply Rstar_n with y; Auto with sets. Qed. Theorem Rstar_contains_Rplus : diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index 6b1e763de..f7278ba2a 100755 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -47,20 +47,20 @@ Theorem Strong_confluence : (U: Type) (R: (Relation U)) (Strongly_confluent U R) -> (Confluent U R). Proof. Intros U R H'; Red. -(Intro x; Red); Intros a b H'0. +Intro x; Red; Intros a b H'0. Unfold 1 coherent. Generalize b; Clear b. Elim H'0; Clear H'0. Intros x0 b H'1; Exists b; Auto with sets. Intros x0 y z H'1 H'2 H'3 b H'4. -(Generalize (Lemma1 U R); Intro h; LApply h; +Generalize (Lemma1 U R); Intro h; LApply h; [Intro H'0; Generalize (H'0 x0 b); Intro h0; LApply h0; [Intro H'5; Generalize (H'5 y); Intro h1; LApply h1; [Intro h2; Elim h2; Intros z0 h3; Elim h3; Intros H'6 H'7; - Clear h h0 h1 h2 h3 | Clear h h0 h1] | Clear h h0] | Clear h]); Auto with sets. -(Generalize (H'3 z0); Intro h; LApply h; + Clear h h0 h1 h2 h3 | Clear h h0 h1] | Clear h h0] | Clear h]; Auto with sets. +Generalize (H'3 z0); Intro h; LApply h; [Intro h0; Elim h0; Intros z1 h1; Elim h1; Intros H'8 H'9; Clear h h0 h1 | - Clear h]); Auto with sets. + Clear h]; Auto with sets. Exists z1; Split; Auto with sets. Apply Rstar_n with z0; Auto with sets. Qed. @@ -69,7 +69,7 @@ Theorem Strong_confluence_direct : (U: Type) (R: (Relation U)) (Strongly_confluent U R) -> (Confluent U R). Proof. Intros U R H'; Red. -(Intro x; Red); Intros a b H'0. +Intro x; Red; Intros a b H'0. Unfold 1 coherent. Generalize b; Clear b. Elim H'0; Clear H'0. @@ -77,9 +77,9 @@ Intros x0 b H'1; Exists b; Auto with sets. Intros x0 y z H'1 H'2 H'3 b H'4. Cut (exT U [t: U] (Rstar U R y t) /\ (R b t)). Intro h; Elim h; Intros t h0; Elim h0; Intros H'0 H'5; Clear h h0. -(Generalize (H'3 t); Intro h; LApply h; +Generalize (H'3 t); Intro h; LApply h; [Intro h0; Elim h0; Intros z0 h1; Elim h1; Intros H'6 H'7; Clear h h0 h1 | - Clear h]); Auto with sets. + Clear h]; Auto with sets. Exists z0; Split; [Assumption | Idtac]. Apply Rstar_n with t; Auto with sets. Generalize H'1; Generalize y; Clear H'1. @@ -87,13 +87,13 @@ Elim H'4. Intros x1 y0 H'0; Exists y0; Auto with sets. Intros x1 y0 z0 H'0 H'1 H'5 y1 H'6. Red in H'. -(Generalize (H' x1 y0 y1); Intro h; LApply h; +Generalize (H' x1 y0 y1); Intro h; LApply h; [Intro H'7; LApply H'7; [Intro h0; Elim h0; Intros z1 h1; Elim h1; Intros H'8 H'9; Clear h H'7 h0 h1 | - Clear h] | Clear h]); Auto with sets. -(Generalize (H'5 z1); Intro h; LApply h; + Clear h] | Clear h]; Auto with sets. +Generalize (H'5 z1); Intro h; LApply h; [Intro h0; Elim h0; Intros t h1; Elim h1; Intros H'7 H'10; Clear h h0 h1 | - Clear h]); Auto with sets. + Clear h]; Auto with sets. Exists t; Split; Auto with sets. Apply Rstar_n with z1; Auto with sets. Qed. @@ -111,40 +111,40 @@ Theorem Newman : (U: Type) (R: (Relation U)) (Noetherian U R) -> (Locally_confluent U R) -> (Confluent U R). Proof. -(Intros U R H' H'0; Red); Intro x. +Intros U R H' H'0; Red; Intro x. Elim (H' x); Unfold confluent. Intros x0 H'1 H'2 y z H'3 H'4. -(Generalize (Rstar_cases U R x0 y); Intro h; LApply h; +Generalize (Rstar_cases U R x0 y); Intro h; LApply h; [Intro h0; Elim h0; [Clear h h0; Intro h1 | Intro h1; Elim h1; Intros u h2; Elim h2; Intros H'5 H'6; Clear h h0 h1 h2] | - Clear h]); Auto with sets. + Clear h]; Auto with sets. Elim h1; Auto with sets. -(Generalize (Rstar_cases U R x0 z); Intro h; LApply h; +Generalize (Rstar_cases U R x0 z); Intro h; LApply h; [Intro h0; Elim h0; [Clear h h0; Intro h1 | Intro h1; Elim h1; Intros v h2; Elim h2; Intros H'7 H'8; Clear h h0 h1 h2] | - Clear h]); Auto with sets. + Clear h]; Auto with sets. Elim h1; Generalize coherent_symmetric; Intro t; Red in t; Auto with sets. Unfold Locally_confluent locally_confluent coherent in H'0. -(Generalize (H'0 x0 u v); Intro h; LApply h; +Generalize (H'0 x0 u v); Intro h; LApply h; [Intro H'9; LApply H'9; [Intro h0; Elim h0; Intros t h1; Elim h1; Intros H'10 H'11; - Clear h H'9 h0 h1 | Clear h] | Clear h]); Auto with sets. + Clear h H'9 h0 h1 | Clear h] | Clear h]; Auto with sets. Clear H'0. Unfold 1 coherent in H'2. -(Generalize (H'2 u); Intro h; LApply h; +Generalize (H'2 u); Intro h; LApply h; [Intro H'0; Generalize (H'0 y t); Intro h0; LApply h0; [Intro H'9; LApply H'9; [Intro h1; Elim h1; Intros y1 h2; Elim h2; Intros H'12 H'13; - Clear h h0 H'9 h1 h2 | Clear h h0] | Clear h h0] | Clear h]); Auto with sets. + Clear h h0 H'9 h1 h2 | Clear h h0] | Clear h h0] | Clear h]; Auto with sets. Generalize Rstar_transitive; Intro T; Red in T. -(Generalize (H'2 v); Intro h; LApply h; +Generalize (H'2 v); Intro h; LApply h; [Intro H'9; Generalize (H'9 y1 z); Intro h0; LApply h0; [Intro H'14; LApply H'14; [Intro h1; Elim h1; Intros z1 h2; Elim h2; Intros H'15 H'16; - Clear h h0 H'14 h1 h2 | Clear h h0] | Clear h h0] | Clear h]); Auto with sets. -Red; (Exists z1; Split); Auto with sets. + Clear h h0 H'14 h1 h2 | Clear h h0] | Clear h h0] | Clear h]; Auto with sets. +Red; '(Exists z1; Split); Auto with sets. Apply T with y1; Auto with sets. Apply T with t; Auto with sets. Qed. -- cgit v1.2.3