diff options
Diffstat (limited to 'coq/example.v')
-rw-r--r-- | coq/example.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/coq/example.v b/coq/example.v index f482f2ab..939f89c9 100644 --- a/coq/example.v +++ b/coq/example.v @@ -6,7 +6,7 @@ Module Example. -Goal forall (A B:Prop),(A /\ B) -> (B /\ A). +Goal forall (A B:Prop),(A /\ B) -> (B /\ A). intros A B. intros H. elim H. @@ -16,6 +16,3 @@ Goal forall (A B:Prop),(A /\ B) -> (B /\ A). Save and_comms. End Example. - - - |