diff options
-rw-r--r-- | coq/example.v | 16 | ||||
-rw-r--r-- | doc/ProofGeneral.texi | 6 |
2 files changed, 13 insertions, 9 deletions
diff --git a/coq/example.v b/coq/example.v index 5c6894c7..27ccd26d 100644 --- a/coq/example.v +++ b/coq/example.v @@ -6,13 +6,13 @@ Module Example. -Goal forall (A B:Prop),(A /\ B) -> (B /\ A). - intros A B. - intros H. - elim H. - split. - assumption. - assumption. -Save and_comms. + Lemma and_commutative : forall (A B:Prop),(A /\ B) -> (B /\ A). + Proof. + intros A B H. + destruct H. + split. + trivial. + trivial. + Qed. End Example. diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 13399c17..2341c1d0 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -667,8 +667,10 @@ Isabelle for more details. @b{Shell Proof General} for shell scripts (not really a proof assistant!)@* @xref{Shell Proof General}, for more details. @end itemize + Proof General is designed to be generic, so if you know how to write regular expressions, you can make: + @itemize @bullet @item @b{Your Proof General} for your favourite proof assistant.@* @@ -676,6 +678,7 @@ For more details of how to make Proof General work with another proof assistant, see the accompanying manual @i{Adapting Proof General}. @end itemize + The exact list of Proof Assistants supported may vary according to the version of Proof General you have and its local configuration; only the standard instances documented in this manual are listed above. @@ -797,7 +800,8 @@ menus. @item First, start Emacs with Proof General loaded. According to how you have installed Proof General, this may be by typing -@code{proofgeneral}, selecting it from a menu, or simply by starting +@code{proofgeneral} in a terminal, +selecting it from a menu, or simply by starting Emacs itself. @item Next, find a new file by @kbd{C-x C-f} and typing as the filename |