--- a/auto-proof.rst	Wed May 13 16:47:07 2009 +0300
+++ b/auto-proof.rst	Wed May 13 16:47:28 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)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/blog.rst	Wed May 13 16:47:28 2009 +0300
@@ -0,0 +1,7 @@
+-*- outline -*-
+
+* Blogspot and Emacs.
+
+See
+
+  http://code.google.com/p/e-blog/

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cmd.rst	Wed May 13 16:47:28 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

--- a/date.rst	Wed May 13 16:47:07 2009 +0300
+++ b/date.rst	Wed May 13 16:47:28 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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/iso-9660.rst	Wed May 13 16:47:28 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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/mail.rst	Wed May 13 16:47:28 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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/svn.rst	Wed May 13 16:47:28 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

--- a/video-file.rst	Wed May 13 16:47:07 2009 +0300
+++ b/video-file.rst	Wed May 13 16:47:28 2009 +0300
@@ -14,6 +14,10 @@
 
 Then do:
 
+  $ ffmpeg -i test.3gp -f mpegvideo -ar 44100 -ac 1 -acodec mp3 test.mpg
+
+  $  for i in `ls -1 *.3gp | cut -d. -f1`; do ffmpeg -y -i $i.3gp -sameq -f mpegvideo -s cif -r 25 -ar 32000 -ac 1 mpegs/$i.mpg; done
+
   $ ffmpeg -i video-in.3gp -b 250 -s 160×120 -r 15 -f avi -an video-out.avi
 or
   $ mencoder -oac mp3lame -ovc lavc -o video-out.avi -vf pp,2xsai,scale video-in.3gp
@@ -21,3 +25,20 @@
   $ mencoder -o video-in.avi -vf pp,2xsai,scale -ovc lavc video-out.3gp
 or
   $ mencoder -o video-in.avi -vf rotate=2 -oac pcm -ovc divx4 video-out.3gp
+
+
+You need to compile FFmpeg with AMR support (--enable-amr_nb
+--enable-amr_wb)
+
+AMR WB FLOAT NOTICE ! Make sure you have downloaded TS26.204
+V5.1.0 from
+http://www.3gpp.org/ftp/Specs/archive/26_series/26.204/26204-510.zip
+and extracted the source to libavcodec/amrwb_float
+
+
+AMR NB FLOAT NOTICE ! Make sure you have downloaded TS26.104
+REL-5 V5.1.0 from
+http://www.3gpp.org/ftp/Specs/latest/Rel-5/26_series/26104-5??.zip
+and extracted the source to libavcodec/amr_float
+and if u try this on an alpha, u may need to change Word32 to int in
+amr/typedef.h

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/virtualization.rst	Wed May 13 16:47:28 2009 +0300
@@ -0,0 +1,11 @@
+-*- outline -*-
+
+* VirtualBox.
+
+x86 virtualization solution.
+
+In Debian Etch use backport repo.
+
+  $ sudo apt-get install virtualbox-ose
+
+