From 9c318584622e1bb50c20d40c60d10231b789b629 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 17 Dec 2020 10:30:43 +0100 Subject: Shorten/improve intro of "Basic proof writing" chapter. --- doc/sphinx/proofs/writing-proofs/index.rst | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst index 7724d7433c..63ddbd0a3a 100644 --- a/doc/sphinx/proofs/writing-proofs/index.rst +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -10,19 +10,16 @@ the user and the assistant. The building blocks for this dialog are tactics which the user will use to represent steps in the proof of a theorem. -Incomplete proofs have one or more open (unproven) sub-goals. Each -goal has its own context (a set of assumptions that can be used to -prove the goal). Tactics can transform goals and contexts. -Internally, the incomplete proof is represented as a partial proof -term, with holes for the unproven sub-goals. +The first section presents the proof mode (the core mechanism of the +dialog between the user and the proof assistant). Then, several +sections describe the available tactics. One section covers the +SSReflect proof language, which provides a consistent alternative set +of tactics to the standard basic tactics. The last section documents +the ``Scheme`` family of commands, which can be used to extend the +power of the :tacn:`induction` and :tacn:`inversion` tactics. -When a proof is complete, the user leaves the proof mode and defers -the verification of the resulting proof term to the :ref:`kernel -`. - -This chapter is divided in several parts, describing the basic ideas -of the proof mode (during which tactics can be used), and several -flavors of tactics, including the SSReflect proof language. +Additional tactics are documented in the next chapter +:ref:`automatic-tactics`. .. toctree:: :maxdepth: 1 -- cgit v1.2.3