aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/example.v
diff options
context:
space:
mode:
Diffstat (limited to 'coq/example.v')
-rw-r--r--coq/example.v10
1 files changed, 5 insertions, 5 deletions
diff --git a/coq/example.v b/coq/example.v
index 1155e5f7..010248a6 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -6,10 +6,10 @@
Goal (A,B:Prop)(A /\ B) -> (B /\ A).
-Intros A B H.
-Induction H.
-Apply conj.
-Assumption.
-Assumption.
+ Intros A B H.
+ Induction H.
+ Apply conj.
+ Assumption.
+ Assumption.
Save and_comms.