--- a/auto-proof.rst Wed Apr 08 21:06:41 2009 +0300
+++ b/auto-proof.rst Mon Apr 13 18:57:03 2009 +0300
@@ -39,11 +39,29 @@
* IsarMathLib.
+The goal of the project is to create a library of formalized mathematics,
+similar to the Mizar Mathematical Library, but written for the Isabelle/Isar
+theorem prover (ZF logic).
+
+See
+
+ http://savannah.nongnu.org/projects/isarmathlib
+ http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
+
+** http://isarmathlib.org/
+
This site is an experimental HTML rendering of fragments of the IsarMathLib
project. IsarMathLib is a library of mathematical proofs formally verified by
the Isabelle theorem proving environment. The formalization is based on the
Zermelo-Fraenkel set theory.
+** Tiddly Formal Math.
+
+This site is an experimental TiddlyWiki rendering of fragments of the
+IsarMathLib project. IsarMathLib is a library of mathematical proofs formally
+verified by the Isabelle theorem proving environment. The formalization is
+based on the Zermelo-Fraenkel set theory.
+
See
- http://isarmathlib.org/
+ http://formalmath.tiddlyspot.com/
--- a/bluetooth.rst Wed Apr 08 21:06:41 2009 +0300
+++ b/bluetooth.rst Mon Apr 13 18:57:03 2009 +0300
@@ -3,11 +3,96 @@
* Debian.
$ sudo apt-get install bluetooth
+ $ sudo apt-get install bluez-utils
* BlueZ.
BlueZ is official Linux Bluetooth protocol stack.
+** How find local bluetooth device?
+
+ $ hcitool dev
+Devices:
+ hci0 00:03:C9:05:65:98
+ hci1 00:1F:81:00:02:5A
+
+or
+
+ $ sudo hciconfig -a
+hci0: Type: USB
+ BD Address: 00:03:C9:05:65:98 ACL MTU: 1017:8 SCO MTU: 64:0
+ UP RUNNING PSCAN
+ RX bytes:2517 acl:12 sco:0 events:64 errors:0
+ TX bytes:756 acl:12 sco:0 commands:33 errors:0
+ Features: 0xff 0xff 0x8d 0xfe 0x9b 0xfd 0x00 0x80
+ Packet type: DM1 DM3 DM5 DH1 DH3 DH5 HV1 HV2 HV3
+ Link policy: RSWITCH HOLD SNIFF PARK
+ Link mode: SLAVE ACCEPT
+ Name: 'desktop-0'
+ Class: 0x3e0100
+ Service Classes: Networking, Rendering, Capturing, Object Transfer, Audio
+ Device Class: Computer, Uncategorized
+ HCI Ver: 2.0 (0x3) HCI Rev: 0x2000 LMP Ver: 2.0 (0x3) LMP Subver: 0x415c
+ Manufacturer: Broadcom Corporation (15)
+
+hci1: Type: USB
+ BD Address: 00:1F:81:00:02:5A ACL MTU: 339:6 SCO MTU: 180:1
+ UP RUNNING PSCAN
+ RX bytes:398 acl:0 sco:0 events:18 errors:0
+ TX bytes:317 acl:0 sco:0 commands:17 errors:0
+ Features: 0xef 0x3e 0x09 0xf0 0x0b 0x08 0x00 0x00
+ Packet type: DM1 DM3 DM5 DH1 DH3 DH5 HV1 HV2 HV3
+ Link policy: RSWITCH HOLD SNIFF PARK
+ Link mode: SLAVE ACCEPT
+ Name: 'desktop-1'
+ Class: 0x3e0100
+ Service Classes: Networking, Rendering, Capturing, Object Transfer, Audio
+ Device Class: Computer, Uncategorized
+ HCI Ver: 1.2 (0x2) HCI Rev: 0x2 LMP Ver: 1.2 (0x2) LMP Subver: 0x2
+ Manufacturer: not assigned (74)
+
+** How find remote bluetooth device?
+
+ $ hcitool scan
+Scanning ...
+ 00:22:66:D1:B7:20 Nokia 5320
+
+** What version of Bluetooth support local device?
+
+ $ sudo hciconfig -a
+hci0: Type: USB
+...
+ HCI Ver: 2.0 (0x3) HCI Rev: 0x2000 LMP Ver: 2.0 (0x3) LMP Subver: 0x415c
+...
+hci1: Type: USB
+...
+ HCI Ver: 1.2 (0x2) HCI Rev: 0x2 LMP Ver: 1.2 (0x2) LMP Subver: 0x2
+...
+
+** What support remote device?
+
+ $ sudo sdptool browse 00:22:66:D1:B7:20
+
+Browsing 00:22:66:D1:B7:20 ...
+Service Name: AVRCP Target
+Service Description: Audio Video Remote Control
+Service Provider: Symbian Software Ltd.
+Service RecHandle: 0x10000
+Service Class ID List:
+ "AV Remote Target" (0x110c)
+Protocol Descriptor List:
+ "L2CAP" (0x0100)
+ PSM: 23
+ "AVCTP" (0x0017)
+ uint16: 0x100
+Profile Descriptor List:
+ "AV Remote" (0x110e)
+ Version: 0x0100
+...
+
+00:1b:52:a8:f6:96
+
+
See
http://www.bluez.org/
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/forth.rst Mon Apr 13 18:57:03 2009 +0300
@@ -0,0 +1,15 @@
+
+* Forth Foundation Library (FFL).
+
+Data types Collections Hash & RNG Interfaces Development Compound
+Bit Array Array CRC-32 Interval Timer ANS Structures Text Input Stream
+Character Single Linked List MD-5 Argument Parser Escaped String Text Output Stream
+Dynamic String Double Linked List SHA-1 Gettexts mo-file Enumeration Regular Expressions
+Character Set Hash Table SHA-256 XML/HTML Parser String Table XML-DOM
+Date Time Binary Tree Mersenne Twister XML/HTML Writer Unit Test DateTime Output Stream
+Complex Number AVL Tree Distributed Message Catalog
+Fraction N-Tree
+
+See
+
+ http://ffl.dvoudheusden.net/index.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/haskell.rst Mon Apr 13 18:57:03 2009 +0300
@@ -0,0 +1,6 @@
+-*- outline -*-
+
+* Installing.
+
+ $ sudo apt-get install ghc6
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/typing.rst Mon Apr 13 18:57:03 2009 +0300
@@ -0,0 +1,9 @@
+-*- outline -*-
+
+* Which software use?
+
+ $ sudo apt-get install gtypist
+
+or
+
+ $ sudo apt-get install tuxtype