@@ -1,6 +1,12 @@
1−***************************
1+***************************************
2−Interactive Theorem Proving
2+DEPRECATED: Interactive Theorem Proving
3−***************************
3+***************************************
6+ **Interactive theorem-proving has been deprecated.**
7+ Support for tactic-based theorem proving will eventually be removed from
9+ Existing tactic-based proofs should be rewritten to use ``rewrite`` instead.
5Idris also supports interactive theorem proving via tactics. This
11Idris also supports interactive theorem proving via tactics. This
6is generally not recommended to be used directly, but rather used as a
12is generally not recommended to be used directly, but rather used as a