diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2000-06-08 19:45:31 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2000-06-08 19:45:31 +0000 |
| commit | 8177e644bc6792bab7db9c384c89cd49edb9c21d (patch) | |
| tree | 0b0685633a2f2424160ce3d5b8458b002a378efa /coq/example.v | |
| parent | 16ec26fb7f102aa37c9546d95f0f61109699a6be (diff) | |
proper indentation;
Diffstat (limited to 'coq/example.v')
| -rw-r--r-- | coq/example.v | 10 |
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. |