7.1 Syntax of tactics and tacticals

http://pauillac.inria.fr/coq/doc/node.1...

Size:5 Kb

7.2 Explicit proof as a term

http://pauillac.inria.fr/coq/doc/node.1...

Size:3 Kb

7.11 Automatizing

http://pauillac.inria.fr/coq/doc/node.1...

Size:12 Kb

7.12 Developing certified program

http://pauillac.inria.fr/coq/doc/node.1...

Size:3 Kb

7.13 The hints list for Auto and EAuto

http://pauillac.inria.fr/coq/doc/node.1...

Size:6 Kb

7.14 Tacticals

http://pauillac.inria.fr/coq/doc/node.1...

Size:6 Kb

7.15 Generation of induction principles..

http://pauillac.inria.fr/coq/doc/node.1...

Size:3 Kb

7.16 A Simple way to define tactic macr..

http://pauillac.inria.fr/coq/doc/node.1...

Size:3 Kb

7.3 Basics

http://pauillac.inria.fr/coq/doc/node.1...

Size:14 Kb

7.4 Negation and contradiction

http://pauillac.inria.fr/coq/doc/node.1...

Size:2 Kb

7.5 Conversion tactics

http://pauillac.inria.fr/coq/doc/node.1...

Size:14 Kb

7.6 Introductions

http://pauillac.inria.fr/coq/doc/node.1...

Size:4 Kb

7.7 Eliminations (Induction and Case An..

http://pauillac.inria.fr/coq/doc/node.1...

Size:12 Kb

7.8 Equality

http://pauillac.inria.fr/coq/doc/node.1...

Size:7 Kb

7.9 Equality and inductive sets

http://pauillac.inria.fr/coq/doc/node.1...

Size:13 Kb

7.10 Inversion

http://pauillac.inria.fr/coq/doc/node.1...

Size:8 Kb

Chapter 7: Tactics

http://pauillac.inria.fr/coq/doc/node.1...

Size:6 Kb

8.1 Refine

http://pauillac.inria.fr/coq/doc/node.1...

Size:5 Kb

8.2 EApply

http://pauillac.inria.fr/coq/doc/node.1...

Size:5 Kb

8.3 Scheme

http://pauillac.inria.fr/coq/doc/node.1...

Size:6 Kb