--- a/auto-proof.rst	Thu Apr 16 10:46:54 2009 +0300
+++ b/auto-proof.rst	Sat Apr 18 12:45:27 2009 +0300
@@ -1,5 +1,12 @@
 -*- outline -*-
 
+* Info/links.
+
+See
+
+  http://en.wikipedia.org/wiki/Automated_theorem_proving
+
+
 * proofgeneral.
 
   $ sudo apt-get install proofgeneral
@@ -65,3 +72,87 @@
 See
 
   http://formalmath.tiddlyspot.com/
+
+* ACL2.
+
+ACL2 (A Computational Logic for Applicative Common Lisp) is a software system
+consisting of a programming language, an extensible theory in a first-order
+logic, and a mechanical theorem prover. ACL2 is designed to support automated
+reasoning in inductive logical theories, mostly for the purpose of software
+and hardware verification. The input language and implementation of ACL2 are
+built on Common Lisp. ACL2 is free, open source (GPL) software.
+
+  $ sudo apt-get install acl2
+
+See
+
+  http://www.cs.utexas.edu/users/moore/acl2/
+  http://en.wikipedia.org/wiki/ACL2
+
+* PVS Specification and Verification System
+
+Old (1992). Many article in 199x.
+
+The system is implemented in Common Lisp, and is released under the GNU
+General Public License (GPL).
+
+See
+
+  http://pvs.csl.sri.com/
+  http://en.wikipedia.org/wiki/Prototype_Verification_System
+  http://www-formal.stanford.edu/clt/ARS/Entries/pvs
+
+* The TPTP Problem Library for Automated Theorem Proving.
+
+The TPTP (Thousands of Problems for Theorem Provers) is a library of test
+problems for automated theorem proving (ATP) systems. The TPTP supplies the
+ATP community with:
+
+ * A comprehensive library of the ATP test problems that are available today,
+   in order to provide an overview and a simple, unambiguous reference
+   mechanism.
+ * A comprehensive list of references and other interesting information for
+   each problem.
+ * Arbitrary size instances of generic problems (e.g., the N-queens problem).
+ * A utility to convert the problems to existing ATP systems' formats.
+ * General guidelines outlining the requirements for ATP system evaluation.
+ * Standards for input and output for ATP systems.
+
+The principal motivation for the TPTP is to support the testing and evaluation
+of ATP systems, to help ensure that performance results accurately reflect the
+capabilities of the ATP system being considered. A common library of problems
+is necessary for meaningful system evaluations, meaningful system comparisons,
+repeatability of testing, and the production of statistically significant
+results. The TPTP is such a library.
+
+See
+
+  http://www.cs.miami.edu/~tptp/
+
+* SPASS.
+
+An Automated Theorem Prover for First-Order Logic with Equality.
+
+See
+
+  http://www.spass-prover.org/index.html
+
+* Competition.
+
+See
+
+  http://www.cs.miami.edu/~tptp/CASC/
+  http://www.cs.albany.edu/~nvm/cade.html
+
+* Conference.
+
+IJCAR is a series of conferences on the topics of automated reasoning,
+automated deduction, and related fields. It is organized semi-regularly as a
+merger of other meetings. IJCAR replaces those independent conferences in the
+years it takes place. The conference is organized by CADE Inc., and CADE has
+always been one of the conferences partaking in IJCAR.
+
+See
+
+  http://www.ijcar.org/
+  http://en.wikipedia.org/wiki/International_Joint_Conference_on_Automated_Reasoning

--- a/bluetooth.rst	Thu Apr 16 10:46:54 2009 +0300
+++ b/bluetooth.rst	Sat Apr 18 12:45:27 2009 +0300
@@ -97,3 +97,10 @@
 
   http://www.bluez.org/
     bluez home page
+
+* Spec.
+
+See
+
+  http://www.bluetooth.com/Bluetooth/Technology/Building/Specifications/
+

--- a/emacs.rst	Thu Apr 16 10:46:54 2009 +0300
+++ b/emacs.rst	Sat Apr 18 12:45:27 2009 +0300
@@ -7,25 +7,28 @@
 know about line numbers and files – it just knows an error happened, and
 that’s it.
 
-You have several options:
+** Binary Search.
 
-  * Binary Search – select half of the file in a region, and M-x eval-region.
-  Depending on whether that causes the error or not, split this half or the
-  other half again, and repeat.
+Select half of the file in a region, and M-x eval-region. Depending on whether
+that causes the error or not, split this half or the other half again, and
+repeat.
+
+** Elisp.
 
-  * Simplified Binary Search – add (error “No error until here”) in the
-  middle of your file. If you get the error “No error until here” when
-  reloading the file, move the expression towards the back of the file,
-  otherwise towards the front of the file.
+ - Use a keyboard macro that moves forward one expression (sexp) and evaluates
+   it.
+ - Try C-x check-parens.
+ - Set (setq debug-on-error t).
+
+** CLI.
 
-  * Use a keyboard macro that moves forward one expression (sexp) and
-  evaluates it.
+  $ emacs --no-init-file --no-site-file --debug-init
+
+** Simplified Binary Search.
 
-  * Try the command line switch --debug-init.
-
-  * Should n’t (setq debug-on-error t) help?
-
- * Try check-parens.
+Add (error “No error until here”) in the middle of your file. If you get the
+error “No error until here” when reloading the file, move the expression
+towards the back of the file, otherwise towards the front of the file.
 
 * Using edebug.
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/javascript.rst	Sat Apr 18 12:45:27 2009 +0300
@@ -0,0 +1,17 @@
+-*- outline -*-
+
+* Inline in HTML.
+
+  <html>
+    <h1>Hello!<h1/>
+    <script language="JavaScript">
+      <!--
+      alert("Hello!")
+      document.write("sin(10) = " + Math.sin(10))
+      //-->
+    </script>
+  </html>
+
+* Hot calc by Firefox.
+
+At URI type some thing like "javascript: 4+5"