tag:blogger.com,1999:blog-114707872024-03-05T04:36:20.421-08:00Isabelle - MAC OSX - Virtual Box required searches during my daily work, collected for referenceAnonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.comBlogger18125tag:blogger.com,1999:blog-11470787.post-6631109474665967992015-10-07T08:31:00.000-07:002015-10-07T08:33:54.791-07:00<div dir="ltr" style="text-align: left;" trbidi="on">
<h2 style="background-color: white; border: 0px; color: #444444; font-stretch: inherit; letter-spacing: -1px; line-height: 1.3em; margin: 0px 0px 10px; padding: 0px; text-align: left; vertical-align: baseline; word-wrap: break-word;">
<span style="font-family: Verdana, sans-serif; font-size: small;"> Raspberry Pi Webmin Install & Updates Via apt-get</span></h2>
<div>
http://c-mobberley.com/wordpress/2013/12/24/raspberry-pi-webmin-install-updates-via-apt-get/</div>
</div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-87573824097143112462015-10-07T07:30:00.002-07:002015-10-07T08:33:05.602-07:00<div dir="ltr" style="text-align: left;" trbidi="on">
<h2 style="background-color: white; box-sizing: border-box; color: #1a1a1a; font-family: 'Open Sans', Helvetica, Arial, sans-serif; line-height: 32px; margin: 0px 0px 6px; text-align: left;">
<span style="font-size: large;"> Auto running programs during Raspberry PI startup</span></h2>
<br />
http://www.raspberry-projects.com/pi/pi-operating-systems/raspbian/auto-running-programs</div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-68929045927093845612015-10-07T07:02:00.003-07:002015-10-07T08:33:43.550-07:00<div dir="ltr" style="text-align: left;" trbidi="on">
<h2 style="background-color: white; box-sizing: border-box; color: #333333; line-height: 1; margin: 0px 0px 10px; padding: 0px; text-align: left;">
<span style="font-family: Verdana, sans-serif; font-size: small;">Setting up a Raspberry Pi as a WiFi access point</span></h2>
<br />
https://learn.adafruit.com/setting-up-a-raspberry-pi-as-a-wifi-access-point/install-software</div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-68396048878964573932015-10-07T07:00:00.002-07:002015-10-07T07:04:07.903-07:00<div dir="ltr" style="text-align: left;" trbidi="on">
<span style="background-color: white; color: #404040; font-family: Roboto, arial, sans-serif; line-height: 18.2px;"><b>Install Webmin in Raspberry PI</b></span><br />
<span style="background-color: white; color: #404040; font-family: Roboto, arial, sans-serif; font-size: 13px; line-height: 18.2px;"><b><br /></b></span>
<br />
<span style="background-color: white; color: #404040; font-family: Roboto, arial, sans-serif; font-size: 13px; line-height: 18.2px;">sudo wget </span><a class="ot-anchor aaTEdf" dir="ltr" href="http://prdownloads.sourceforge.net/webadmin/webmin-1.580.tar.gz" jslog="10929; track:click" rel="nofollow" style="background-color: white; color: #427fed; cursor: pointer; font-family: Roboto, arial, sans-serif; font-size: 13px; line-height: 18.2px; text-decoration: none; transition: color 0.218s;" target="_blank">http://prdownloads.sourceforge.net/webadmin/webmin-1.580.tar.gz</a><br /><span style="background-color: white; color: #404040; font-family: Roboto, arial, sans-serif; font-size: 13px; line-height: 18.2px;">sudo tar -zxvf webmin-1.580.tar.gz </span><br />
<span style="background-color: white; color: #404040; font-family: Roboto, arial, sans-serif; font-size: 13px; line-height: 18.2px;">sudo mkdir /var/www/webmin </span><br />
<span style="background-color: white; color: #404040; font-family: Roboto, arial, sans-serif; font-size: 13px; line-height: 18.2px;">cd webmin-1.580 </span><br />
<span style="background-color: white; color: #404040; font-family: Roboto, arial, sans-serif; font-size: 13px; line-height: 18.2px;">sudo sh setup.sh /var/www/webmin </span><br />
<br />
<span style="background-color: white; color: #404040; font-family: Roboto, arial, sans-serif; font-size: 13px; line-height: 18.2px;">The above commands are available at:</span><br />
<span style="background-color: white; font-size: 13px; line-height: 18.2px;"><span style="color: #404040; font-family: Roboto, arial, sans-serif;">http://pastebin.com/stUvKNLX</span></span><br />
<span style="background-color: white; font-size: 13px; line-height: 18.2px;"><span style="color: #404040; font-family: Roboto, arial, sans-serif;"><br /></span></span>
<span style="background-color: white; font-size: 13px; line-height: 18.2px;"><span style="color: #404040; font-family: Roboto, arial, sans-serif;">An instruction video is available at:</span></span><br />
<span style="background-color: white; font-size: 13px; line-height: 18.2px;"><span style="color: #404040; font-family: Roboto, arial, sans-serif;">https://www.youtube.com/watch?v=VYSulADwLAk</span></span></div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-38473012957038178982015-09-08T07:51:00.005-07:002015-09-08T07:51:59.625-07:00Mount a host folder inside a VirtualBox ubuntu guest<div dir="ltr" style="text-align: left;" trbidi="on">
<div style="background: rgb(255, 255, 255); border: 0px; color: #333333; font-family: Georgia, 'Bitstream Charter', serif; font-size: 16px; line-height: 24px; margin-bottom: 24px; padding: 0px; vertical-align: baseline;">
To mount a host folder inside a VirtualBox ubuntu guest, you have to create a <em style="background: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">mounpoint</em>, that is, a directory in your Ubuntu which will reflect the shared folder from Windows:</div>
<div style="background: rgb(255, 255, 255); border: 0px; color: #333333; font-family: Georgia, 'Bitstream Charter', serif; font-size: 16px; line-height: 24px; margin-bottom: 24px; padding: 0px; vertical-align: baseline;">
<code style="background: transparent; border: 0px; font-family: Monaco, Consolas, 'Andale Mono', 'DejaVu Sans Mono', monospace; font-size: 13px; margin: 0px; padding: 0px; vertical-align: baseline;"># sudo mkdir /media/windows-share</code></div>
<div style="background: rgb(255, 255, 255); border: 0px; color: #333333; font-family: Georgia, 'Bitstream Charter', serif; font-size: 16px; line-height: 24px; margin-bottom: 24px; padding: 0px; vertical-align: baseline;">
Of course you may choose an alternative path for your mountpoint. With your mountpoint created you can now mount the shared folder, like this:</div>
<div style="background: rgb(255, 255, 255); border: 0px; color: #333333; font-family: Georgia, 'Bitstream Charter', serif; font-size: 16px; line-height: 24px; margin-bottom: 24px; padding: 0px; vertical-align: baseline;">
<code style="background: transparent; border: 0px; font-family: Monaco, Consolas, 'Andale Mono', 'DejaVu Sans Mono', monospace; font-size: 13px; margin: 0px; padding: 0px; vertical-align: baseline;"># sudo mount -t vboxsf <em style="background: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">folder-name</em> /media/windows-share</code></div>
<div style="background: rgb(255, 255, 255); border: 0px; color: #333333; font-family: Georgia, 'Bitstream Charter', serif; font-size: 16px; line-height: 24px; margin-bottom: 24px; padding: 0px; vertical-align: baseline;">
Where <em style="background: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">folder-name<strong style="background: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </strong></em>will be the name you assigned for this folder when you were adding it in the shared folders list.</div>
<div style="background: rgb(255, 255, 255); border: 0px; color: #333333; font-family: Georgia, 'Bitstream Charter', serif; font-size: 16px; line-height: 24px; margin-bottom: 24px; padding: 0px; vertical-align: baseline;">
You could use the <em style="background: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">/etc/init.d/rc.local</em> script to execute these commands on startup to have the shared folders automatically mounted every time you start your Ubuntu VirtualBox.</div>
<div style="background: rgb(255, 255, 255); border: 0px; margin-bottom: 24px; padding: 0px; vertical-align: baseline;">
<span style="color: #333333; font-family: Georgia, Bitstream Charter, serif;"><span style="line-height: 24px;">http://www.giannistsakiris.com/2008/04/09/virtualbox-access-windows-host-shared-folders-from-ubuntu-guest/</span></span></div>
</div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-7671913180395285572014-10-13T04:07:00.000-07:002014-10-13T04:07:15.614-07:00Installing Z/EVES on Mac OS X<div dir="ltr" style="text-align: left;" trbidi="on">
The following article is written by Andrius Velykis. The full link for the article is found below.<br />
<br />
<a href="http://www.springerlink.com/content/w96x54254l852272/" style="-webkit-transition: color 0.1s ease-in, background 0.1s ease-in; background: rgb(255, 255, 255); box-sizing: border-box; color: #1abc9c; font-family: Montserrat, sans-serif; font-size: 16px; line-height: 28px; text-decoration: none; transition: color 0.1s ease-in, background 0.1s ease-in; word-wrap: break-word;">Z/EVES</a><span style="background-color: white; color: #555555; font-family: Montserrat, sans-serif; font-size: 16px; line-height: 28px;"> is an interactive theorem prover for </span><a href="http://en.wikipedia.org/wiki/Z_notation" style="-webkit-transition: color 0.1s ease-in, background 0.1s ease-in; background: rgb(255, 255, 255); box-sizing: border-box; color: #1abc9c; font-family: Montserrat, sans-serif; font-size: 16px; line-height: 28px; text-decoration: none; transition: color 0.1s ease-in, background 0.1s ease-in; word-wrap: break-word;">Z notation</a><span style="background-color: white; color: #555555; font-family: Montserrat, sans-serif; font-size: 16px; line-height: 28px;">. It can be used to develop Z specifications and reason about them. It has a number of attractive features, such as an easier learning curve (in comparison to related theorem provers, e.g. </span><a href="http://isabelle.in.tum.de/" style="-webkit-transition: color 0.1s ease-in, background 0.1s ease-in; background: rgb(255, 255, 255); box-sizing: border-box; color: #1abc9c; font-family: Montserrat, sans-serif; font-size: 16px; line-height: 28px; text-decoration: none; transition: color 0.1s ease-in, background 0.1s ease-in; word-wrap: break-word;">Isabelle</a><span style="background-color: white; color: #555555; font-family: Montserrat, sans-serif; font-size: 16px; line-height: 28px;">), powerful proof tactics, and the ability to do proofs in Z notation.</span><br />
<span style="background-color: white; color: #555555; font-family: Montserrat, sans-serif; font-size: 16px; line-height: 28px;"><br /></span>
http://andrius.velykis.lt/2012/09/installing-zeves-on-mac-os-x/</div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-47967917169848564432014-10-04T12:33:00.001-07:002014-10-04T12:33:50.750-07:00How to Create a Bootable Windows 7 USB Installer on a Mac<iframe allowfullscreen="" frameborder="0" height="270" src="https://www.youtube.com/embed/8z1gqw0ougo" width="480"></iframe>Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-63536199948176639522013-11-07T23:51:00.000-08:002013-11-08T01:07:11.921-08:00Isabelle Keyword Dictionary<div dir="ltr" style="text-align: left;" trbidi="on">
<u><b><a href="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013/doc/isar-ref.pdf" target="_blank">Isabelle/Isar Reference Manual</a></b></u><br />
For a comprehensive guide on Isabelle commands<br />
<u><b><br /></b></u>
<b><u>declare </u></b><i><u>thms</u> - </i>declares theorems to the current local theory context. No theorem binding is involved here, unlike theorems or lemmas (cf.§5.11), so declare only has the efect of applying attributes as included in the theorem speci cation. <span style="font-size: x-small;"><a href="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013/doc/isar-ref.pdf" target="_blank">Isar manual p85</a></span><br />
<b><u><br /></u></b>
<u><b>Locales </b>- A sectioning concept for Isabelle</u><br />
Locales are a means to de fine local scopes for the interactive proving process of the theorem prover Isabelle. They delimit a range in which fixed assumption are made, and theorems are proved that depend on these assumptions. A locale may also contain constants de fined locally and associated with pretty printing syntax. Locales can be seen as a simple form of modules. <a href="http://wwwbroy.in.tum.de/~wenzelm/papers/Locales-TPHOLs99.pdf" target="_blank">read more</a><br />
<br />
<u><b>Recursive Functions</b> - Defining Recursive Functions in Isabelle/HOL</u><br />
This tutorial describes the use of the new function package, which<br />
provides general recursive function de nitions for Isabelle/HOL. We start<br />
with very simple examples and then gradually move on to more advanced<br />
topics such as manual termination proofs, nested recursion, partiality, tail<br />
recursion and congruence rules. <a href="http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013/doc/functions.pdf" target="_blank">read tutorial</a><br />
<br />
<br /></div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-42617517333832782892013-10-22T03:31:00.001-07:002013-10-22T03:31:26.897-07:00Change uuid of harddrive in VirtualBox<div dir="ltr" style="text-align: left;" trbidi="on">
When you remove a hard disk from a Virtual PC you cannot put it back into the same Virtual PC. Hence you have to change the UUID of the hard disk before you can attach it to the same Virtual PC. You can do it by issuing the following command:<br />
<br />
<span style="font-family: Courier New, Courier, monospace;">VBoxManage internalcommands sethduuid disk2.vdi </span></div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-17348115450829547262013-04-18T15:30:00.001-07:002013-04-18T15:30:09.237-07:00To enable NTFS copying and modification rights in Mac<div dir="ltr" style="text-align: left;" trbidi="on">
Install <a href="http://sourceforge.net/projects/catacombae/files/NTFS-3G%20for%20Mac%20OS%20X/2010.10.2/ntfs-3g-2010.10.2-macosx.dmg/download" style="background-color: white; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px; text-decoration: none;"><span style="color: orange;">NTFS-3G for Mac OS X 2010.10.2</span></a><br />
<span style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;"><br /></span>
<span style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;">Then, you should follow these steps in order to have the latest version of MacFuse:</span><br style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;" /><span style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;">1) Install http://macfuse.googlecode.com/files/MacFUSE-2.0.3%2C2.dmg - RESTART</span><br style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;" /><span style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;">2) Install http://www.tuxera.com/mac/macfuse-core-10.5-2.1.9.dmg - RESTART</span><br style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;" /><span style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;">3) Install http://content.wuala.com/contents/grahamperrin/public/2010/07/31/a/MacFUSE.prefPane-2.0-64-bit-2009-09-10.zip?dl=1</span><br style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;" /><br style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;" /><span style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;">Now you have the latest version of MacFuse and the 64bit prefpane.</span><br />
<span style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;"><br /></span>
<span style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;"><br /></span>
<span style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;">Link to <a href="http://macntfs-3g.blogspot.co.uk/2010/10/ntfs-3g-for-mac-os-x-2010102.html" target="_blank">original blogspot</a></span><br />
<span style="background-color: white; color: #333333; font-family: Georgia, serif; font-size: 13px; line-height: 20.796875px;"><br /></span></div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-50271512735491163302013-04-18T10:19:00.002-07:002013-04-18T10:22:19.353-07:00Wordpress : “You do not have sufficient permissions to access this page” after you change database prefix <div dir="ltr" style="text-align: left;" trbidi="on">
<span style="font-family: Verdana, sans-serif; font-size: x-small;"><br /></span>
<br />
<div style="background-color: white; border: 0px; clear: both; line-height: 18px; margin-bottom: 1em; padding: 0px; vertical-align: baseline; word-wrap: break-word;">
<span style="font-family: Verdana, sans-serif; font-size: x-small;">Have you changed the prefix of your database tables? I'm 90% sure, that this is your problem.</span></div>
<div style="background-color: white; border: 0px; clear: both; line-height: 18px; margin-bottom: 1em; padding: 0px; vertical-align: baseline; word-wrap: break-word;">
<span style="font-family: Verdana, sans-serif; font-size: x-small;">The thing is that WordPress uses the <code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 1px 5px; vertical-align: baseline;">$table_prefix</code> variable for forming the option and usermeta keys names, where it's storing the roles and capabilities information. So once you change the prefix, but don't update your db, you get this error. Here's how to fix it - execute this SQL command through phpMyAdmin, or a different interface for interacting with your DB(you can do it with PHP as well):</span></div>
<pre class="default prettyprint prettyprinted" style="background-color: #eeeeee; border: 0px; line-height: 18px; margin-bottom: 10px; max-height: 600px; overflow: auto; padding: 5px; vertical-align: baseline; width: auto;"><code style="border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"><span style="font-family: Courier New, Courier, monospace; font-size: x-small;"><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">UPDATE </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`{%TABLE_PREFIX%}usermeta`</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> SET </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`meta_key`</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">=</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> replace</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">(</span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`meta_key`</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">,</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">'{%OLD_TABLE_PREFIX%}'</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">,</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">'{%NEW_TABLE_PREFIX%}'</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">);</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">
UPDATE </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`{%TABLE_PREFIX%}options`</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> SET </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`option_name`</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">=</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> replace</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">(</span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`option_name`</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">,</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">'{%OLD_TABLE_PREFIX%}'</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">,</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">'{%NEW_TABLE_PREFIX%}'</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">);</span></span></code></pre>
<div style="background-color: white; border: 0px; clear: both; line-height: 18px; margin-bottom: 1em; padding: 0px; vertical-align: baseline; word-wrap: break-word;">
<span style="font-family: Verdana, sans-serif; font-size: x-small;">Where:</span></div>
<ul style="background-color: white; border: 0px; font-family: Arial, 'Liberation Sans', 'DejaVu Sans', sans-serif; font-size: 14px; line-height: 18px; list-style-image: initial; list-style-position: initial; margin: 0px 0px 1em 30px; padding: 0px; vertical-align: baseline;">
<li style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline; word-wrap: break-word;"><span style="font-family: Verdana, sans-serif; font-size: x-small;"><code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">{%TABLE_PREFIX%}</code> is your current <code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">$table_prefix</code>(as set in <code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">wp-config.php</code>)</span></li>
<li style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline; word-wrap: break-word;"><span style="font-family: Verdana, sans-serif; font-size: x-small;"><code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">{%OLD_TABLE_PREFIX%}</code> is your previous <code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">$table_prefix</code></span></li>
<li style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline; word-wrap: break-word;"><span style="font-family: Verdana, sans-serif; font-size: x-small;"><code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">{%NEW_TABLE_PREFIX%}</code> is your new(current) <code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">$table_prefix</code> - it will most-likely be the same as your <code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">{%TABLE_PREFIX%}</code>.</span></li>
</ul>
<div style="background-color: white; border: 0px; clear: both; line-height: 18px; margin-bottom: 1em; padding: 0px; vertical-align: baseline; word-wrap: break-word;">
<span style="font-family: Verdana, sans-serif; font-size: x-small;">So if your old <code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 1px 5px; vertical-align: baseline;">$table_prefix</code> was <code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 1px 5px; vertical-align: baseline;">wp_test_</code> and your new one is <code style="background-color: #eeeeee; border: 0px; margin: 0px; padding: 1px 5px; vertical-align: baseline;">wp_</code>, you would do this query:</span></div>
<pre class="default prettyprint prettyprinted" style="background-color: #eeeeee; border: 0px; line-height: 18px; margin-bottom: 10px; max-height: 600px; overflow: auto; padding: 5px; vertical-align: baseline; width: auto;"><code style="border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"><span style="font-family: Courier New, Courier, monospace; font-size: x-small;"><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">UPDATE </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`wp_usermeta`</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> SET </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`meta_key`</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">=</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> replace</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">(</span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`meta_key`</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">,</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">'wp_test_'</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">,</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">'wp_'</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">);</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">
UPDATE </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`wp_options`</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> SET </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`option_name`</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">=</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> replace</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">(</span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">`option_name`</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">,</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">'wp_test_'</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">,</span><span class="pln" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"> </span><span class="str" style="background-color: transparent; border: 0px; color: maroon; margin: 0px; padding: 0px; vertical-align: baseline;">'wp_'</span><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">);</span></span></code></pre>
<pre class="default prettyprint prettyprinted" style="background-color: #eeeeee; border: 0px; line-height: 18px; margin-bottom: 10px; max-height: 600px; overflow: auto; padding: 5px; vertical-align: baseline; width: auto;"><code style="border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;"><span class="pun" style="background-color: transparent; border: 0px; font-family: Verdana, sans-serif; font-size: x-small; margin: 0px; padding: 0px; vertical-align: baseline;"><i>Link to the <a href="http://stackoverflow.com/questions/13815461/you-do-not-have-sufficient-permissions-to-access-this-page-without-any-change" target="_blank">Original Post</a>!!!</i></span></code></pre>
<pre class="default prettyprint prettyprinted" style="background-color: #eeeeee; border: 0px; font-family: Consolas, Menlo, Monaco, 'Lucida Console', 'Liberation Mono', 'DejaVu Sans Mono', 'Bitstream Vera Sans Mono', 'Courier New', monospace, serif; font-size: 14px; line-height: 18px; margin-bottom: 10px; max-height: 600px; overflow: auto; padding: 5px; vertical-align: baseline; width: auto;"><code style="border: 0px; font-family: Consolas, Menlo, Monaco, 'Lucida Console', 'Liberation Mono', 'DejaVu Sans Mono', 'Bitstream Vera Sans Mono', 'Courier New', monospace, serif; margin: 0px; padding: 0px; vertical-align: baseline;"><span class="pun" style="background-color: transparent; border: 0px; margin: 0px; padding: 0px; vertical-align: baseline;">
</span></code></pre>
</div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-35656203692868833472013-03-20T08:22:00.002-07:002013-03-20T08:22:19.347-07:00Formal Logic Symbols<div dir="ltr" style="text-align: left;" trbidi="on">
<img alt="\models" class="tex" src="http://upload.wikimedia.org/math/e/7/6/e766ce0de4bbe899d7ea2ebe40b3e0ee.png" style="background-color: white; border: none; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px; margin: 0px; vertical-align: middle;" /><span style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;"> </span><b style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;">double turnstile</b><br />
<span style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;">In </span><a href="http://en.wikipedia.org/wiki/Logic" style="background-color: white; background-image: none; color: #0b0080; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px; text-decoration: none;" title="Logic">logic</a><span style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;">, the </span><a href="http://en.wikipedia.org/wiki/Symbol_(formal)" style="background-color: white; background-image: none; color: #0b0080; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px; text-decoration: none;" title="Symbol (formal)">symbol</a><span style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;"> </span><img alt="\vDash" class="tex" src="http://upload.wikimedia.org/math/c/1/1/c11b72dc7a3b789b717a21f90be06c47.png" style="background-color: white; border: none; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px; margin: 0px; vertical-align: middle;" /><span style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;"> or </span><img alt="\models" class="tex" src="http://upload.wikimedia.org/math/e/7/6/e766ce0de4bbe899d7ea2ebe40b3e0ee.png" style="background-color: white; border: none; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px; margin: 0px; vertical-align: middle;" /><span style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;"> is called the </span><b style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;">double turnstile</b><span style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;">. It is closely related to the </span><a href="http://en.wikipedia.org/wiki/Turnstile_(symbol)" style="background-color: white; background-image: none; color: #0b0080; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px; text-decoration: none;" title="Turnstile (symbol)">turnstile</a><span style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;"> symbol </span><img alt="\vdash" class="tex" src="http://upload.wikimedia.org/math/b/f/7/bf73c9341a48c47c84a48dad635ff940.png" style="background-color: white; border: none; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px; margin: 0px; vertical-align: middle;" /><span style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;">, which has a single bar across the middle. It is often read as "</span><a href="http://en.wikipedia.org/wiki/Logical_consequence" style="background-color: white; background-image: none; color: #0b0080; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px; text-decoration: none;" title="Logical consequence"><i>entails</i></a><span style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;">", "<i>models</i>" or "<i>is a semantic consequence of</i>".</span><br />
<span style="background-color: white; font-family: sans-serif; font-size: 12.800000190734863px; line-height: 19.200000762939453px;"><br /></span></div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-60280845230484066242013-02-28T06:21:00.002-08:002013-02-28T06:21:53.389-08:00How to Take a Screenshot in Mac OS X<div dir="ltr" style="text-align: left;" trbidi="on">
<b>How to Take a Screenshot in Mac OS X</b><br />
http://www.wikihow.com/Take-a-Screenshot-in-Mac-OS-X<br />
<br />
<br />
<b>How To Capture a Screen Shot with Mac OS X</b><br />
<br />
http://graphicssoft.about.com/od/screencapturemac/ht/macscreenshot.htm<br />
<br /></div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-4542086181891126252013-02-23T02:11:00.000-08:002013-02-23T02:13:37.469-08:00A Compact Introduction to Isabelle/HOL<div dir="ltr" style="text-align: left;" trbidi="on">
<br />
A Compact Introduction to Isabelle/HOL<br />
<br />
I found <a href="http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/nipkow_sl_4lan.pdf" target="_blank">this tutorial </a>by Tobias to be very useful in understanding isabelle Theorem Prover.<br />
<br />
Further, <a href="http://www.inf.ed.ac.uk/teaching/courses/ar/isabelle/isabelle-startup.pdf" target="_blank">Getting Sarted with isabelle</a>, is for those formalism enthusiasts, who wants to get a first shot at Isabelle Theorem Prover.<br />
<div>
<br /></div>
<div>
<br /></div>
</div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-17061552037287028032013-02-23T01:02:00.004-08:002013-02-23T01:02:30.264-08:00Emacs Commands List <div dir="ltr" style="text-align: left;" trbidi="on">
<span style="font-size: large;"><u>Emacs Commands List </u></span><br />C = Control<br />M = Meta = Alt|Esc<br /><br /><b>Basics</b><code style="font-size: medium;">C-x C-f </code>"find" file i.e. open/create a file in buffer<br /><code style="font-size: medium;">C-x C-s </code>save the file<br /><code style="font-size: medium;">C-x C-w </code>write the text to an alternate name<br /><code style="font-size: medium;">C-x C-v </code>find alternate file<br /><code style="font-size: medium;">C-x i </code>insert file at cursor position<br /><code style="font-size: medium;">C-x b </code>create/switch buffers<br /><code style="font-size: medium;">C-x C-b </code>show buffer list<br /><code style="font-size: medium;">C-x k </code>kill buffer<br /><code style="font-size: medium;">C-z </code>suspend emacs<br /><code style="font-size: medium;">C-X C-c </code>close down emacs<br /><br /><b>Basic movement</b><code style="font-size: medium;">C-f </code>forward char<br /><code style="font-size: medium;">C-b </code>backward char<br /><code style="font-size: medium;">C-p </code>previous line<br /><code style="font-size: medium;">C-n </code>next line<br /><code style="font-size: medium;">M-f </code>forward one word<br /><code style="font-size: medium;">M-b </code>backward one word<br /><code style="font-size: medium;">C-a </code>beginning of line<br /><code style="font-size: medium;">C-e </code>end of line<br /><code style="font-size: medium;">C-v </code>one page up<br /><code style="font-size: medium;">M-v </code>scroll down one page<br /><code style="font-size: medium;">M-< </code>beginning of text<br /><code style="font-size: medium;">M-> </code>end of text<br /><br /><b>Editing</b><br /><code style="font-size: medium;">M-n </code>repeat the following command n times<br /><code style="font-size: medium;">C-u </code>repeat the following command 4 times<br /><code style="font-size: medium;">C-u n </code>repeat n times<br /><code style="font-size: medium;">C-d </code>delete a char<br /><code style="font-size: medium;">M-d </code>delete word<br /><code style="font-size: medium;">M-Del </code>delete word backwards<br /><code style="font-size: medium;">C-k </code>kill line<br /><br /><code style="font-size: medium;">C-Space </code>Set beginning mark (for region marking for example)<br /><code style="font-size: medium;">C-W </code>"kill" (delete) the marked region region<br /><code style="font-size: medium;">M-W </code>copy the marked region<br /><code style="font-size: medium;">C-y </code>"yank" (paste) the copied/killed region/line<br /><code style="font-size: medium;">M-y </code>yank earlier text (cycle through kill buffer)<br /><code style="font-size: medium;">C-x C-x </code>exchange cursor and mark<br /><br /><code style="font-size: medium;">C-t </code>transpose two chars<br /><code style="font-size: medium;">M-t </code>transpose two words<br /><code style="font-size: medium;">C-x C-t </code>transpose lines<br /><code style="font-size: medium;">M-u </code>make letters uppercase in word from cursor position to end<br /><code style="font-size: medium;">M-c </code>simply make first letter in word uppercase<br /><code style="font-size: medium;">M-l </code>opposite to M-u<br /><br /><b>Important</b><code style="font-size: medium;">C-g </code>quit the running/entered command<br /><code style="font-size: medium;">C-x u </code>undo previous action<br /><code style="font-size: medium;">M-x revert-buffer RETURN </code>(insert like this) undo all changes since last save<br /><code style="font-size: medium;">M-x recover-file RETURN </code>Recover text from an autosave-file<br /><code style="font-size: medium;">M-x recover-session RETURN </code>if you edited several files<br /><br /><b>Online-Help</b><code style="font-size: medium;">C-h c </code>which command does this keystroke invoke<br /><code style="font-size: medium;">C-h k </code>which command does this keystroke invoke and what does it do?<br /><code style="font-size: medium;">C-h l </code>what were my last 100 typed keys<br /><code style="font-size: medium;">C-h w </code>what key-combo does this command have?<br /><code style="font-size: medium;">C-h f </code>what does this function do<br /><code style="font-size: medium;">C-h v </code>what's this variable and what is it's value<br /><code style="font-size: medium;">C-h b </code>show all keycommands for this buffer<br /><code style="font-size: medium;">C-h t </code>start the emacs tutorial<br /><code style="font-size: medium;">C-h i </code>start the info reader<br /><code style="font-size: medium;">C-h C-k </code>start up info reader and go to a certain key-combo point<br /><code style="font-size: medium;">C-h F </code>show the emacs FAQ<br /><code style="font-size: medium;">C-h p </code>show infos about the Elisp package on this machine<br /><br /><b>Search/Replace</b><code style="font-size: medium;">C-s </code>Search forward<br /><code style="font-size: medium;">C-r </code>search backward<br /><code style="font-size: medium;">C-g </code>return to where search started (if you are still in search mode)<br /><code style="font-size: medium;">M-% </code>query replace<br />
<blockquote style="font-size: medium;">
<code>Space or y </code>replace this occurence<br /><code>Del or n </code>don't replace<br /><code>. </code>only replace this and exit (replace)<br /><code>, </code>replace and pause (resume with Space or y)<br /><code>! </code>replace all following occurences<br /><code>^ </code>back to previous match<br /><code>RETURN or q </code>quit replace</blockquote>
<br /><b>Search/Replace with regular expressions</b>Characters to use in regular expressions:<br /><code style="font-size: medium;">^ </code>beginning of line<br /><code style="font-size: medium;">$ </code>end of line<br /><code style="font-size: medium;">. </code>single char<br /><code style="font-size: medium;">.* </code>group or null of chars<br /><code style="font-size: medium;">\< </code>beginning of a word<br /><code style="font-size: medium;">\> </code>end of a word<br /><code style="font-size: medium;">[] </code>every char inside the backets (for example [a-z] means every small letter)<br /><br /><code style="font-size: medium;">M C-s RETURN </code>search for regular expression forward<br /><code style="font-size: medium;">M C-r RETURN </code>search for regular expression backward<br /><code style="font-size: medium;">M C-s </code>incremental search<br /><code style="font-size: medium;">C-s </code>repeat incremental search<br /><code style="font-size: medium;">M C-r </code>incremental search backwards<br /><code style="font-size: medium;">C-r </code>repeat backwards<br /><code style="font-size: medium;">M-x query-replace-regexp </code>search and replace<br /><br /><b>Window-Commands</b><code style="font-size: medium;">C-x 2 </code>split window vertically<br /><code style="font-size: medium;">C-x o </code>change to other window<br /><code style="font-size: medium;">C-x 0 </code>delete window<br /><code style="font-size: medium;">C-x 1 </code>close all windows except the one the cursors in<br /><code style="font-size: medium;">C-x ^ </code>enlarge window<br /><code style="font-size: medium;">M-x shrink-window </code>command says it ;-)<br /><code style="font-size: medium;">M C-v </code>scroll other window<br /><code style="font-size: medium;">C-x 4 f </code>find file in other window<br /><code style="font-size: medium;">C-x 4 o </code>change to other window<br /><code style="font-size: medium;">C-x 4 0 </code>kill buffer and window<br /><code style="font-size: medium;">C-x 5 2 </code>make new frame<br /><code style="font-size: medium;">C-x 5 f </code>find file in other frame<br /><code style="font-size: medium;">C-x 5 o </code>change to other frame<br /><code style="font-size: medium;">C-x 5 0 </code>close this frame<br /><br /><b>Bookmark commands</b><code style="font-size: medium;">C-x r m </code>set a bookmark at current cursor pos<br /><code style="font-size: medium;">C-x r b </code>jump to bookmark<br /><code style="font-size: medium;">M-x bookmark-rename </code>says it<br /><code style="font-size: medium;">M-x bookmark-delete </code>"<br /><code style="font-size: medium;">M-x bookmark-save</code> "<br /><code style="font-size: medium;">C-x r l </code>list bookmarks<br /><blockquote style="font-size: medium;">
<code>d </code>mark bookmark for deletion<br /><code>r </code>rename bookmark<br /><code>s </code>save all listed bookmarks<br /><code>f </code>show bookmark the cursor is over<br /><code>m </code>mark bookmarks to be shown in multiple window<br /><code>v </code>show marked bookmarks (or the one the cursor is over)<br /><code>t </code>toggle listing of the corresponding paths<br /><code>w </code>" path to this file<br /><code>x </code>delete marked bookmarks<br /><code>Del </code>?<br /><code>q </code>quit bookmark list</blockquote>
<br /><code style="font-size: medium;">M-x bookmark-write </code>write all bookmarks in given file<br /><code style="font-size: medium;">M-x bookmark-load </code>load bookmark from given file<br /><br /><b>Shell</b><br /><code style="font-size: medium;">M-x shell </code>starts shell modus<br /><code style="font-size: medium;">C-c C-c </code>same as C-c under unix (stop running job)<br /><code style="font-size: medium;">C-d </code>delete char forward<br /><code style="font-size: medium;">C-c C-d </code>Send EOF<br /><code style="font-size: medium;">C-c C-z </code>suspend job (C-z under unix)<br /><code style="font-size: medium;">M-p </code>show previous commands<br /><br /><b>DIRectory EDitor (dired)</b><code style="font-size: medium;">C-x d </code>start up dired<br /><code style="font-size: medium;">C </code>(large C) copy<br /><code style="font-size: medium;">d </code>mark for erase<br /><code style="font-size: medium;">D </code>delete right away<br /><code style="font-size: medium;">e or f </code>open file or directory<br /><code style="font-size: medium;">g </code>reread directory structure from file<br /><code style="font-size: medium;">G </code>change group permissions (chgrp)<br /><code style="font-size: medium;">k </code>delete line from listing on screen (don't actually delete)<br /><code style="font-size: medium;">m </code>mark with *<br /><code style="font-size: medium;">n </code>move to next line<br /><code style="font-size: medium;">o </code>open file in other window and go there<br /><code style="font-size: medium;">C-o </code>open file in other window but don't change there<br /><code style="font-size: medium;">P </code>print file<br /><code style="font-size: medium;">q </code>quit dired<br /><code style="font-size: medium;">Q </code>do query-replace in marked files<br /><code style="font-size: medium;">R </code>rename file<br /><code style="font-size: medium;">u </code>remove mark<br /><code style="font-size: medium;">v </code>view file content<br /><code style="font-size: medium;">x </code>delete files marked with D<br /><code style="font-size: medium;">z </code>compress file<br /><code style="font-size: medium;">M-Del </code>remove all marks (whatever kind)<br /><code style="font-size: medium;">~ </code>mark backup files (name~ files) for deletion<br /><code style="font-size: medium;"># </code>mark auto-save files (#name#) for deletion<br /><code style="font-size: medium;">*/ </code>mark directory with * (C-u * removes that mark again)<br /><code style="font-size: medium;">= </code>compare this file with marked file<br /><code style="font-size: medium;">M-= </code>compare this file with it's backup file<br /><code style="font-size: medium;">! </code>apply shell command to this file<br /><code style="font-size: medium;">M-} </code>change to the next file marked with * od D<br /><code style="font-size: medium;">M-{ </code>" previous "<br /><code style="font-size: medium;">% d </code>mark files described through regular expression for deletion<br /><code style="font-size: medium;">% m </code>" (with *)<br /><code style="font-size: medium;">+ </code>create directory<br /><code style="font-size: medium;">> </code>changed to next dir<br /><code style="font-size: medium;">< </code>change to previous dir<br /><code style="font-size: medium;">s </code>toggle between sorting by name or date<br /><br />Maybe into this category also fits this command:<br /><code style="font-size: medium;">M-x speedbar </code>starts up a separate window with a directory view<br /><br /><b>Telnet</b><br /><code style="font-size: medium;">M-x telnet </code>starts up telnet-modus<br /><code style="font-size: medium;">C-d </code>either delete char or send EOF<br /><code style="font-size: medium;">C-c C-c </code>stop running job (similar to C-c under unix)<br /><code style="font-size: medium;">C-c C-d </code>send EOF<br /><code style="font-size: medium;">C-c C-o </code>clear output of last command<br /><code style="font-size: medium;">C-c C-z </code>suspend execution of command<br /><code style="font-size: medium;">C-c C-u </code>kill line backwards<br /><code style="font-size: medium;">M-p </code>recall previous command<br /><br /><b>Text</b><br />Works only in text mode<br /><code style="font-size: medium;">M-s </code>center line<br /><code style="font-size: medium;">M-S </code>center paragraph<br /><code style="font-size: medium;">M-x center-region </code>name says<br /><br /><b>Macro-commands</b><code style="font-size: medium;">C-x ( </code>start macro definition<br /><code style="font-size: medium;">C-x ) </code>end of macro definition<br /><code style="font-size: medium;">C-x e </code>execute last definied macro<br /><code style="font-size: medium;">M-n C-x e </code>execute last defined macro n times<br /><code style="font-size: medium;">M-x name-last-kbd-macro </code>give name to macro (for saving)<br /><code style="font-size: medium;">M-x insert-keyboard-macro </code>save named macro into file<br /><code style="font-size: medium;">M-x load-file </code>load macro<br /><code style="font-size: medium;">M-x macroname </code>execute macroname<br /><br /><b>Programming</b><br /><code style="font-size: medium;">M C-\ </code>indent region between cursor and mark<br /><code style="font-size: medium;">M-m </code>move to first (non-space) char in this line<br /><code style="font-size: medium;">M-^ </code>attach this line to previous<br /><code style="font-size: medium;">M-; </code>formatize and indent comment<br />C, C++ and Java Modes<br /><code style="font-size: medium;">M-a </code>beginning of statement<br /><code style="font-size: medium;">M-e </code>end of statement<br /><code style="font-size: medium;">M C-a </code>beginning of function<br /><code style="font-size: medium;">M C-e </code>end of function<br /><code style="font-size: medium;">C-c RETURN </code>Set cursor to beginning of function and mark at the end<br /><code style="font-size: medium;">C-c C-q </code>indent the whole function according to indention style<br /><code style="font-size: medium;">C-c C-a </code>toggle modus in which after electric signs (like {}:';./*) emacs does the indention<br /><code style="font-size: medium;">C-c C-d </code>toggle auto hungry mode in which emacs deletes groups of spaces with one del-press<br /><code style="font-size: medium;">C-c C-u </code>go to beginning of this preprocessor statement<br /><code style="font-size: medium;">C-c C-c </code>comment out marked area<br />More general (I guess)<br /><code style="font-size: medium;">M-x outline-minor-mode </code>collapses function definitions in a file to a mere {...}<br /><code style="font-size: medium;">M-x show-subtree </code>If you are in one of the collapsed functions, this un-collapses it<br />In order to achive some of the feats coming up now you have to run etags *.c *.h *.cpp (or what ever ending you source files have) in the source directory<br /><code style="font-size: medium;">M-. </code>(Thats Meta dot) If you are in a function call, this will take you to it's definition<br /><code style="font-size: medium;">M-x tags-search ENTER </code>Searches through all you etaged<br /><code style="font-size: medium;">M-, </code>(Meta comma) jumps to the next occurence for tags-search<br /><code style="font-size: medium;">M-x tags-query-replace </code>yum. This lets you replace some text in all the tagged files<br /><code></code><br /><br /><b>GDB (Debugger)</b><code style="font-size: medium;">M-x gdb </code>starts up gdm in an extra window<br /><br /><b>Version Control</b><code style="font-size: medium;">C-x v d </code>show all registered files in this dir<br /><code style="font-size: medium;">C-x v = </code>show diff between versions<br /><code style="font-size: medium;">C-x v u </code>remove all changes since last checkin<br /><code style="font-size: medium;">C-x v ~ </code>show certain version in different window<br /><code style="font-size: medium;">C-x v l </code>print log<br /><code style="font-size: medium;">C-x v i </code>mark file for version control add<br /><code style="font-size: medium;">C-x v h </code>insert version control header into file<br /><code style="font-size: medium;">C-x v r </code>check out named snapshot<br /><code style="font-size: medium;">C-x v s </code>create named snapshot<br /><code style="font-size: medium;">C-x v a </code>create changelog file in gnu-style<br /></div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-62925019353275162302013-02-22T03:20:00.001-08:002013-02-23T00:51:10.333-08:00Isabelle Syntax<div dir="ltr" style="text-align: left;" trbidi="on">
<div class="page" title="Page 9">
<div class="section" style="background-color: rgb(100.000000%, 100.000000%, 100.000000%);">
<div class="layoutArea">
<div class="column">
<span style="font-family: Georgia, Times New Roman, serif;"><span style="color: #999999; font-size: x-small;">extract from <a href="http://isabelle.in.tum.de/dist/Isabelle2013/doc/prog-prove.pdf" target="_blank"><i>isabelle- Programming</i></a></span></span></div>
<div class="column">
<span style="font-family: Georgia, Times New Roman, serif;"><span style="font-size: 11.000000pt;"><br /></span></span></div>
<div class="column">
<span style="font-family: Georgia, Times New Roman, serif;"><span style="font-size: large;">Basic Syntax</span></span><br />
<span style="font-family: Georgia, Times New Roman, serif;"><span style="font-size: 11.000000pt;">Most statements of logic (inner-syntax) should be places in
speech-marks
</span></span><br />
<blockquote style="border: none; margin: 0px 0px 0px 40px; padding: 0px;">
<blockquote style="border: none; margin: 0px 0px 0px 40px; padding: 0px;">
<span style="font-family: Courier New, Courier, monospace; font-size: 15px;">"numberMonth n = months!(n - 1)"</span></blockquote>
</blockquote>
<br />
<span style="font-family: Georgia, Times New Roman, serif;"></span><span style="font-family: Georgia, 'Times New Roman', serif; font-size: 11pt;">Isabelle employs L</span><span style="font-family: Georgia, 'Times New Roman', serif; font-size: 8pt; vertical-align: 2pt;">A</span><span style="font-family: Georgia, 'Times New Roman', serif; font-size: 11pt;">T</span><span style="font-family: Georgia, 'Times New Roman', serif; font-size: 11pt; vertical-align: -2pt;">E</span><span style="font-family: Georgia, 'Times New Roman', serif; font-size: 11pt;">X-like tags for unicode syntax </span><br />
<ul style="list-style-type: none; text-align: left;">
<ul>
<li><span style="font-family: Georgia, Times New Roman, serif;"><span style="font-size: 11.000000pt;">e.g.</span><span style="color: rgb(0.000000%, 0.000000%, 100.000000%); font-family: 'CMSY10'; font-size: 11.000000pt;">∀</span><span style="color: rgb(0.000000%, 0.000000%, 100.000000%); font-family: 'CMSSI10'; font-size: 11.000000pt;">x</span><span style="color: rgb(0.000000%, 0.000000%, 100.000000%); font-family: 'CMMI10'; font-size: 11.000000pt;">.</span><span style="color: rgb(0.000000%, 0.000000%, 100.000000%); font-family: 'CMSY10'; font-size: 11.000000pt;">∃</span><span style="color: rgb(0.000000%, 0.000000%, 100.000000%); font-family: 'CMSSI10'; font-size: 11.000000pt;">y</span><span style="color: rgb(0.000000%, 0.000000%, 100.000000%); font-family: 'CMMI10'; font-size: 11.000000pt;">.</span><span style="color: rgb(0.000000%, 0.000000%, 100.000000%); font-family: 'CMSSI10'; font-size: 11.000000pt;">y </span><span style="color: rgb(0.000000%, 0.000000%, 100.000000%); font-family: 'CMMI10'; font-size: 11.000000pt;">> </span><span style="color: rgb(0.000000%, 0.000000%, 100.000000%); font-family: 'CMSSI10'; font-size: 11.000000pt;">x </span><span style="font-size: 11.000000pt;">is written as per L</span><span style="font-size: 8.000000pt; vertical-align: 2.000000pt;">A</span><span style="font-size: 11.000000pt;">T</span><span style="font-size: 11.000000pt; vertical-align: -2.000000pt;">E</span><span style="font-size: 11.000000pt;">X. </span></span></li>
<li><span style="font-family: Courier New, Courier, monospace; font-size: 11pt;">\forall x.\exists y.y > x</span></li>
</ul>
</ul>
<div>
<span style="font-family: Georgia, Times New Roman, serif;"><span style="font-size: 15px;">HOL(</span><i><span style="font-size: 15px;">Higher Order Logic</span></i><span style="font-size: 15px;">) is a typed logic whose type system resembles that of functional programming languages. Thus there are: </span></span><br />
<ul style="text-align: left;">
<li><span style="font-family: Georgia, Times New Roman, serif; font-size: 15px;"><b>base types</b>, in particular bool, the type of truth values, nat, the type of natural numbers (<a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEj5-AV2Si6lwpBNT0agN0vnqP7wywBAB7yrmk1TtnxbjqxRozoSvSAItY0ctCsNZxckvggi1Ol1j1c7HOl_t8Kcy69JFH5AH7ozWBm2Np1TLdpiyQsEmp0wgPqMR_-DY9ZdQr68/s1600/Screen+Shot+2013-02-23+at+08.49.59.png" imageanchor="1" style="font-family: Times; font-size: medium; margin-left: 1em; margin-right: 1em; text-align: center;"><img border="0" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEj5-AV2Si6lwpBNT0agN0vnqP7wywBAB7yrmk1TtnxbjqxRozoSvSAItY0ctCsNZxckvggi1Ol1j1c7HOl_t8Kcy69JFH5AH7ozWBm2Np1TLdpiyQsEmp0wgPqMR_-DY9ZdQr68/s1600/Screen+Shot+2013-02-23+at+08.49.59.png" /></a>), and int, the type of mathematical integers (<a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEim2hbRhP_Mnw1tuTW41MV2b4pznIpgNne1yThCv3YXWk6FCqsYLD_oMnz4Tclma8Nwaz4G5YVSkRKKf-3J1vqMd4yD3iO-qhrGtpIhvZME_C8lM64d8iwMJn9miOTfobqjeCRn/s1600/Screen+Shot+2013-02-23+at+08.49.46.png" imageanchor="1" style="font-family: Times; font-size: medium; margin-left: 1em; margin-right: 1em; text-align: center;"><img border="0" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEim2hbRhP_Mnw1tuTW41MV2b4pznIpgNne1yThCv3YXWk6FCqsYLD_oMnz4Tclma8Nwaz4G5YVSkRKKf-3J1vqMd4yD3iO-qhrGtpIhvZME_C8lM64d8iwMJn9miOTfobqjeCRn/s1600/Screen+Shot+2013-02-23+at+08.49.46.png" /></a>).</span></li>
</ul>
<ul style="text-align: left;">
<li><span style="font-family: Georgia, Times New Roman, serif; font-size: 15px;"><b>type constructors</b>, in particular list, the type of lists, and set, the type of sets. Type constructors are written postfix, e.g. <i><span style="color: blue;">nat list</span></i> is the type of lists whose elements are natural numbers.</span></li>
</ul>
<ul style="text-align: left;">
<li><span style="font-family: Georgia, Times New Roman, serif; font-size: 15px;"><b>function types</b>, denoted by<a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEhjzxbQ_Fx6iCC9cir1HRkJ8L46ha1bdMZGrALN7wCTZJRjwXvM4CinhUNXFQXXATlLt7T-l5KyHCVi8Lyx_R2Drn766sdOROHmhczPRCs_umqvf33gUWX_Fhw-09A024agsJHa/s1600/Screen+Shot+2013-02-23+at+08.07.51.png" imageanchor="1" style="font-family: Times; font-size: medium; margin-left: 1em; margin-right: 1em; text-align: center;"><img border="0" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEhjzxbQ_Fx6iCC9cir1HRkJ8L46ha1bdMZGrALN7wCTZJRjwXvM4CinhUNXFQXXATlLt7T-l5KyHCVi8Lyx_R2Drn766sdOROHmhczPRCs_umqvf33gUWX_Fhw-09A024agsJHa/s1600/Screen+Shot+2013-02-23+at+08.07.51.png" /></a>.</span></li>
</ul>
<ul style="text-align: left;">
<li><span style="font-family: Georgia, Times New Roman, serif; font-size: 15px;"><b>type variables</b>, denoted by <span style="color: blue;"><i>'</i><i>a, </i><i>'b</i></span> etc., just like in ML</span></li>
</ul>
<b style="font-family: Georgia, 'Times New Roman', serif; font-size: 15px;"><img border="0" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEhva1GbFxqJuAspYx002Sa00cq9OlQi6KgOcjVqrSrOu5D3Wwqqvl5cQFoiN5hp9KL2axBuR7AOApLpEv4zAJYM5TRF8HBVFUuoZuDd9qisv4rIakbNr8wuNPqjmEOKjyNau93T/s1600/Screen+Shot+2013-02-23+at+08.30.02.png" /></b><br />
<ul style="text-align: left;">
<li><span style="font-family: Georgia, Times New Roman, serif;"><span style="font-size: 15px;"><b>Formulae </b>are terms of type bool. There are the basic constants True and</span></span><span style="font-family: Georgia, 'Times New Roman', serif; font-size: 15px;">False and the usual logical connectives (in decreasing order of precedence):</span><span style="font-family: Georgia, 'Times New Roman', serif; font-size: 15px;"><a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEjZfgymtgFX7iAE-INOag7HucZl0izKYd69Pe8juqcLgZiqDbtydrg20xPx6vw1U5QqUlKyF4mh1UGF9n4AY2YrPT0KK-3d9UbSWrV5AA4BZ2dj4N04V_0hJg6ULjXSKzrttYQt/s1600/Screen+Shot+2013-02-23+at+08.28.54.png" imageanchor="1" style="font-family: Times; font-size: medium; margin-left: 1em; margin-right: 1em; text-align: center;"><img border="0" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEjZfgymtgFX7iAE-INOag7HucZl0izKYd69Pe8juqcLgZiqDbtydrg20xPx6vw1U5QqUlKyF4mh1UGF9n4AY2YrPT0KK-3d9UbSWrV5AA4BZ2dj4N04V_0hJg6ULjXSKzrttYQt/s1600/Screen+Shot+2013-02-23+at+08.28.54.png" /></a> </span></li>
</ul>
<a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEjM0KMnbavsAM3-c7x-jkuRbTWAL7BIhqEgOn6RA9adSe_2AzYyHiD519WSlUoPeF9mOdpqYptGIrajCOfbbc3vtj8iaQNAUBQOVdyj7bZEb-iZTo4uMOj3Gupfik6dsKtU_NCo/s1600/Screen+Shot+2013-02-23+at+08.31.51.png" imageanchor="1" style="margin-left: 1em; margin-right: 1em; text-align: center;"><img border="0" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEjM0KMnbavsAM3-c7x-jkuRbTWAL7BIhqEgOn6RA9adSe_2AzYyHiD519WSlUoPeF9mOdpqYptGIrajCOfbbc3vtj8iaQNAUBQOVdyj7bZEb-iZTo4uMOj3Gupfik6dsKtU_NCo/s1600/Screen+Shot+2013-02-23+at+08.31.51.png" /></a></div>
<div>
<br /></div>
<div>
<br />
<br />
<span style="font-family: Georgia, Times New Roman, serif; font-size: large;">Theories</span><br />
<span style="font-family: Georgia, Times New Roman, serif;">Roughly speaking, a theory is a named collection of types, functions, and </span><span style="font-family: Georgia, 'Times New Roman', serif;">theorems, much like a module in a programming language. All the Isabelle </span><span style="font-family: Georgia, 'Times New Roman', serif;">text that you ever type needs to go into a theory. The general format of a</span><br />
<span style="font-family: Georgia, Times New Roman, serif;"> </span><br />
<span style="font-family: Georgia, Times New Roman, serif;"><i> <b>theory</b> T is</i></span><br />
<i><span style="font-family: Georgia, 'Times New Roman', serif;"> </span><span style="font-family: Georgia, Times New Roman, serif;"><b>theory</b> T</span></i><br />
<i><span style="font-family: Georgia, 'Times New Roman', serif;"> </span><span style="font-family: Georgia, Times New Roman, serif;"><b>imports</b> T1 : : : T n</span></i><br />
<i><span style="font-family: Georgia, 'Times New Roman', serif;"> </span><span style="font-family: Georgia, Times New Roman, serif;"><b>begin</b></span></i><br />
<i><span style="font-family: Georgia, 'Times New Roman', serif;"> </span><span style="font-family: Georgia, 'Times New Roman', serif;"> </span><span style="font-family: Georgia, 'Times New Roman', serif;">definitions, theorems and proofs</span></i><br />
<i><span style="font-family: Georgia, 'Times New Roman', serif;"> </span><span style="font-family: Georgia, Times New Roman, serif;"><b>end</b></span></i><br />
<span style="font-family: Georgia, Times New Roman, serif;"><br /></span>
<span style="font-family: Georgia, Times New Roman, serif;">where <i>T1</i> : : : <i>T n</i> are the names of existing theories that <i>T</i> is based on. The </span><i style="font-family: Georgia, 'Times New Roman', serif;">Ti </i><span style="font-family: Georgia, 'Times New Roman', serif;">are the direct parent theories of </span><i style="font-family: Georgia, 'Times New Roman', serif;">T</i><span style="font-family: Georgia, 'Times New Roman', serif;">. Everything defined in the parent theories </span><span style="font-family: Georgia, Times New Roman, serif;">(and their parents, recursively) is automatically visible. Each theory <i>T</i> must </span><span style="font-family: Georgia, 'Times New Roman', serif;">reside in a theory file named T:thy.</span></div>
</div>
</div>
</div>
</div>
</div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-52675932115311650692013-02-22T03:07:00.001-08:002013-02-22T03:17:39.574-08:00Installing Isabelle Theorem Prover<div dir="ltr" style="text-align: left;" trbidi="on">
<span style="font-family: Courier New, Courier, monospace;"><br /></span>
<u><span style="font-family: Courier New, Courier, monospace;"><b>Introduction to Isabelle </b>[<span style="font-size: x-small;">ref: <i><a href="http://en.wikipedia.org/wiki/Isabelle_(proof_assistant)" target="_blank">wikipedia</a>, <a href="http://www-users.cs.york.ac.uk/~simonf/Isabelle/" target="_blank">York University</a></i></span>],</span></u><br />
<span style="font-family: Courier New, Courier, monospace;"><span style="background-color: white; line-height: 19.18402862548828px;"><br /></span></span>
<br />
<div class="separator" style="clear: both; text-align: center;">
<a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgAnvaVnhndR7GwBVDw0BRrIP4IJ26KQxtRjzCU7VRLgaRD0cOlYNKoGKvMEwKeoSp1LBxOs6O7q5dB6Q3nxW9LWovZ1joYtcZK_JzeynSosZChaWDb-GE2w1G-NxRM1zMTM2ke/s1600/isabelle_logo.gif" imageanchor="1" style="margin-left: 1em; margin-right: 1em;"><span style="font-family: Courier New, Courier, monospace;"><img border="0" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgAnvaVnhndR7GwBVDw0BRrIP4IJ26KQxtRjzCU7VRLgaRD0cOlYNKoGKvMEwKeoSp1LBxOs6O7q5dB6Q3nxW9LWovZ1joYtcZK_JzeynSosZChaWDb-GE2w1G-NxRM1zMTM2ke/s1600/isabelle_logo.gif" /></span></a></div>
<span style="font-family: Courier New, Courier, monospace;"><span style="background-color: white; line-height: 19.18402862548828px;"><br /></span></span>
<span style="font-family: Courier New, Courier, monospace;"><span style="background-color: white; line-height: 19.18402862548828px;">The </span><b style="background-color: white; line-height: 19.18402862548828px;">Isabelle theorem prover</b><span style="background-color: white; line-height: 19.18402862548828px;"> is an </span><a href="http://en.wikipedia.org/wiki/Proof_assistant" style="background-color: white; background-image: none; color: #0b0080; line-height: 19.18402862548828px; text-decoration: initial;" title="Proof assistant">interactive theorem prover</a><span style="background-color: white; line-height: 19.18402862548828px;">, successor of the </span><a class="mw-redirect" href="http://en.wikipedia.org/wiki/HOL_theorem_prover" style="background-color: white; background-image: none; color: #0b0080; line-height: 19.18402862548828px; text-decoration: initial;" title="HOL theorem prover">Higher Order Logic (HOL) theorem prover</a><span style="background-color: white; line-height: 19.18402862548828px;">. It is an </span><a class="mw-redirect" href="http://en.wikipedia.org/wiki/LCF_theorem_prover" style="background-color: white; background-image: none; color: #0b0080; line-height: 19.18402862548828px; text-decoration: initial;" title="LCF theorem prover">LCF-style</a><span style="background-color: white; line-height: 19.18402862548828px;"> theorem prover (written in </span><a href="http://en.wikipedia.org/wiki/Standard_ML" style="background-color: white; background-image: none; color: #0b0080; line-height: 19.18402862548828px; text-decoration: initial;" title="Standard ML">Standard ML</a><span style="background-color: white; line-height: 19.18402862548828px;">), so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic (a weak </span><a href="http://en.wikipedia.org/wiki/Type_theory" style="background-color: white; background-image: none; color: #0b0080; line-height: 19.18402862548828px; text-decoration: initial;" title="Type theory">type theory</a><span style="background-color: white; line-height: 19.18402862548828px;">), which is used to encode object logics like </span><a href="http://en.wikipedia.org/wiki/First-order_logic" style="background-color: white; background-image: none; color: #0b0080; line-height: 19.18402862548828px; text-decoration: initial;" title="First-order logic">First-order logic</a><span style="background-color: white; line-height: 19.18402862548828px;"> (FOL), </span><a href="http://en.wikipedia.org/wiki/Higher-order_logic" style="background-color: white; background-image: none; color: #0b0080; line-height: 19.18402862548828px; text-decoration: initial;" title="Higher-order logic">Higher-order logic (HOL)</a><span style="background-color: white; line-height: 19.18402862548828px;"> or </span><a href="http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory" style="background-color: white; background-image: none; color: #0b0080; line-height: 19.18402862548828px; text-decoration: initial;" title="Zermelo–Fraenkel set theory">Zermelo–Fraenkel set theory</a><span style="background-color: white; line-height: 19.18402862548828px;"> </span></span><br />
<span style="background-color: white;"><span style="font-family: Courier New, Courier, monospace;"><br /></span></span>
<span style="font-family: Courier New, Courier, monospace;"><span style="background-color: white; line-height: 19.171875px;">Isabelle consists of t</span><span style="background-color: white;">wo components: the </span><span style="background-color: white; color: red;">proof engine </span><span style="background-color: white;">and </span><span style="background-color: white; color: red;">user interface</span><span style="background-color: white;"><span style="color: #3333b3;">.</span></span></span><br />
<br />
<div class="page" title="Page 4">
<div class="section" style="background-color: rgb(100.000000%, 100.000000%, 100.000000%);">
<div class="layoutArea">
<div class="column">
<span style="background-color: white; font-family: 'Courier New', Courier, monospace; line-height: 19.171875px;">Isabelle has s</span><span style="font-family: Courier New, Courier, monospace;">everal interfaces available:</span><br />
<span style="font-family: 'Courier New', Courier, monospace;"></span><br />
<ul style="list-style-type: none; text-align: left;"><span style="font-family: 'Courier New', Courier, monospace;">
<li>Proof General (emacs) <span style="color: blue;">[included] </span></li>
<li>PIDE (jEdit) <span style="color: blue;">[included]</span></li>
<li><span style="font-family: 'Courier New', Courier, monospace;">I3P (Netbeans) </span></li>
</span></ul>
<span style="font-family: 'Courier New', Courier, monospace;">
</span><br />
<div style="text-align: left;">
<span style="font-family: Courier New, Courier, monospace;">I just started using isabelle 3 weeks ago and according to advice from Simon Foster I'm sticking with Emacs interface for now.</span></div>
<div style="text-align: left;">
<span style="font-family: Courier New, Courier, monospace;"><br /></span></div>
<div style="text-align: left;">
<span style="font-family: Courier New, Courier, monospace;"><b>Download</b> <a href="http://www.cl.cam.ac.uk/research/hvg/Isabelle/" target="_blank">Isabelle</a></span></div>
<div style="text-align: left;">
<br /></div>
<div style="text-align: left;">
</div>
<div class="p1">
<u><span style="font-family: Courier New, Courier, monospace;">Some Shortcuts in Emacs</span></u></div>
<div class="p1">
<span style="font-family: Courier New, Courier, monospace;">Ctrl C + N -> next line in proof checking</span></div>
<div class="p1">
<span style="font-family: Courier New, Courier, monospace;">Ctrl C + U -> previous line in proof checking</span></div>
<div class="p2">
<span style="font-family: Courier New, Courier, monospace;"><br /></span></div>
<div class="p1">
<span style="font-family: Courier New, Courier, monospace;">Ctrl C + Ctrl Enter -> go to position</span></div>
<div class="p1">
<span style="font-family: Courier New, Courier, monospace;">Ctrl C + A + S -> sledge hammer</span></div>
<br />
<br />
<ol></ol>
<ul style="list-style-type: none;">
</ul>
</div>
</div>
</div>
</div>
</div>
Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0tag:blogger.com,1999:blog-11470787.post-73030269442582502672011-11-22T03:22:00.000-08:002011-11-22T03:27:02.602-08:00Using OpenSSL for secure communication in IIS6 in a Windows 2003 environment1. Install OpenSSL<br /><br />2. Go to the OpenSSL prompt and create the necessary keys with the following commands.<br /><br />genrsa -des3 -out server.key 2048 <br /><br />req -new -key server.key -out server.csr -config C:\OpenSSL-Win32\bin\openssl.cfg -batch<br /><br />genrsa -des3 -out ca.key 2048<br /><br />req -new -x509 -days 365 -key ca.key -out ca.crt -config C:\OpenSSL-Win32\bin\openssl.cfg -batch<br /><br />x509 -req -days 365 -in server.csr -CA ca.crt -CAkey ca.key -set_serial 01 -out server.crt -extensions usr_cert -extfile C:\OpenSSL-Win32\bin\openssl.cfg <br /><br />pkcs12 -export -in server.crt -inkey server.key -out server.pfx -name "MyTestCert"<br /><br /><br />3. Place the server.pfx in the 'Default Web Site' Directory Security in IIS.<br /><br /><br />4. Import the necessary Certificates to every client PC either manually by:<br /><br />a. Import ca.crt to client PC's Certificate Store, inside "Trusted Root Certificate Authorities".<br />b. Import server.crt to client PC's Certificate Store, inside "Intermediate Certification Authorities".<br />c. Import server.crt to client PC's Certificate Store, inside "Trusted Publishers".Anonymoushttp://www.blogger.com/profile/09876656796883722385noreply@blogger.com0