# HG changeset patch
# User Oleksandr Gavenko <gavenkoa@gmail.com>
# Date 1241726367 -10800
# Node ID aab18e67e03bcc5d9df6aa8bfb110e44b4ee4d8e
# Parent  0c37d729555fd0efe581a0f7a380e07053356af4# Parent  551a197b656b14d913f7b9d83a0a21d0e5f3a0c5
merge

diff -r 0c37d729555f -r aab18e67e03b auto-proof.rst
--- a/auto-proof.rst	Thu May 07 12:50:06 2009 +0300
+++ b/auto-proof.rst	Thu May 07 22:59:27 2009 +0300
@@ -73,6 +73,22 @@
 
   http://formalmath.tiddlyspot.com/
 
+* HOL Light.
+
+HOL Light is a computer program to help users prove interesting mathematical
+theorems completely formally in higher order logic. It sets a very exacting
+standard of correctness, but provides a number of automated tools and
+pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and
+real analysis) to save the user work. It is also fully programmable, so users
+can extend it with new theorems and inference rules without compromising its
+soundness.
+
+Ocalm.
+
+See
+
+  http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html
+
 * ACL2.
 
 ACL2 (A Computational Logic for Applicative Common Lisp) is a software system
@@ -156,3 +172,12 @@
 
   http://www.ijcar.org/
   http://en.wikipedia.org/wiki/International_Joint_Conference_on_Automated_Reasoning
+
+* Top 100.
+
+  http://www.cs.ru.nl/~freek/100/
+                (winner)
+  http://personal.stevens.edu/~nkahl/Top100Theorems.html
+                (orig list)
+  http://www.cse.unsw.edu.au/~kleing/top100/#5
+                (Isabelle)
diff -r 0c37d729555f -r aab18e67e03b blog.rst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/blog.rst	Thu May 07 22:59:27 2009 +0300
@@ -0,0 +1,7 @@
+-*- outline -*-
+
+* Blogspot and Emacs.
+
+See
+
+  http://code.google.com/p/e-blog/
diff -r 0c37d729555f -r aab18e67e03b cmd.rst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cmd.rst	Thu May 07 22:59:27 2009 +0300
@@ -0,0 +1,9 @@
+-*- outline -*-
+
+* CMD tricks.
+
+  $ set /p TOOLOUTPUT= < temp.txt
+
+  $ for /f "tokens=*" %%i in ('%~dp0sometool.exe') do set TOOLOUTPUT=%%i
+
+  $ for /f "tokens=1 delims=" %%s in (users.txt) do (echo %%S & command "%%S") >> outputfile.txt
diff -r 0c37d729555f -r aab18e67e03b date.rst
--- a/date.rst	Thu May 07 12:50:06 2009 +0300
+++ b/date.rst	Thu May 07 22:59:27 2009 +0300
@@ -141,3 +141,7 @@
 Here is that TZ value again, this time on standard output so that you
 can use the /usr/bin/tzselect command in shell scripts:
 Europe/Kiev
+
+** Debian Lenny.
+
+  $ sudo dpkg-reconfigure tzdata
diff -r 0c37d729555f -r aab18e67e03b iso-9660.rst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/iso-9660.rst	Thu May 07 22:59:27 2009 +0300
@@ -0,0 +1,10 @@
+-*- outline -*-
+
+* Mounting ISO Images in Solaris.
+
+  $ /usr/sbin/lofiadm -d /dev/lofi/1
+  $ /usr/sbin/lofiadm -a /var/tmp/CDImage.iso
+  $ [ -d /mnt ] && echo OK || echo FAILURE
+  $ /usr/sbin/umount /mnt
+  $ /usr/sbin/mount -F hsfs -o ro /dev/lofi/1 /mnt
+  $ cd /mnt
diff -r 0c37d729555f -r aab18e67e03b mail.rst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/mail.rst	Thu May 07 22:59:27 2009 +0300
@@ -0,0 +1,31 @@
+-*- outline -*-
+
+* Sending email via gmail in emacs.
+
+; install starttls from here (no need for patch)
+; http://josefsson.org/emacs-smtp-starttls.html
+
+(setq send-mail-function 'smtpmail-send-it
+   message-send-mail-function 'smtpmail-send-it
+   smtpmail-starttls-credentials
+   '(("smtp.gmail.com" 587 nil nil))
+   smtpmail-auth-credentials
+   (expand-file-name "~/.authinfo")
+   smtpmail-default-smtp-server "smtp.gmail.com"
+   smtpmail-smtp-server "smtp.gmail.com"
+   smtpmail-smtp-service 587
+   smtpmail-debug-info t
+   starttls-extra-arguments nil
+   smtpmail-warn-about-unknown-extensions t
+   starttls-use-gnutls nil)
+
+machine smtp.gmail.com login [your name]@gmail.com password [your password]
+
+And finally download, unzip, make and install startttls:
+
+http://josefsson.org/emacs-smtp-starttls.html
+
+See
+
+  http://justinsboringpage.blogspot.com/2009/02/sending-email-via-gmail-in-emacs.html
+  http://obfuscatedcode.wordpress.com/2007/04/26/configuring-emacs-for-gmails-smtp
diff -r 0c37d729555f -r aab18e67e03b svn.rst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/svn.rst	Thu May 07 22:59:27 2009 +0300
@@ -0,0 +1,7 @@
+-*- outline -*-
+
+* Copy repo from SourceForge to GoogleCode.
+
+  $ svnsync init https://PROJ.googlecode.com/svn https://PROJ.svn.sourceforge.net/svnroot/PROJ
+  $ svnsync --username NAME --password PASSWORD \
+                sync https://PROJ.googlecode.com/svn https://PROJ.svn.sourceforge.net/svnroot/PROJ
diff -r 0c37d729555f -r aab18e67e03b virtualization.rst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/virtualization.rst	Thu May 07 22:59:27 2009 +0300
@@ -0,0 +1,11 @@
+-*- outline -*-
+
+* VirtualBox.
+
+x86 virtualization solution.
+
+In Debian Etch use backport repo.
+
+  $ sudo apt-get install virtualbox-ose
+
+