--- 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)
--- /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/
--- /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
--- 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
--- /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
--- /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
--- /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
--- /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
+
+