From ed9f35dd30e87038bb2333a7fa9b7ff75ecb1335 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 2 Apr 2004 17:00:41 +0000 Subject: Use official indentation\! --- coq/example.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'coq/example.v') diff --git a/coq/example.v b/coq/example.v index d9976ea7..cfe85203 100644 --- a/coq/example.v +++ b/coq/example.v @@ -5,10 +5,10 @@ *) Goal (A,B:Prop)(A /\ B) -> (B /\ A). - Intros A B H. - Elim H. - Intros. - Split. - Assumption. - Assumption. + Intros A B H. + Elim H. + Intros. + Split. + Assumption. + Assumption. Save and_comms. -- cgit v1.2.3