Update of /cvsroot/fink/dists/10.4/unstable/main/finkinfo/sci
In directory sc8-pr-cvs5.sourceforge.net:/tmp/cvs-serv9923/main/finkinfo/sci
Modified Files:
mizar-mode.info
Log Message:
Update from tracker
https://sourceforge.net/tracker/index.php?func=detail&aid=1643019&group_id=17203&atid=414256
Index: mizar-mode.info
===================================================================
RCS file: /cvsroot/fink/dists/10.4/unstable/main/finkinfo/sci/mizar-mode.info,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- mizar-mode.info 16 Jan 2007 03:54:03 -0000 1.3
+++ mizar-mode.info 1 Feb 2007 02:44:38 -0000 1.4
@@ -1,9 +1,9 @@
Package: mizar-mode
Description: Work with Mizar files in Emacs
Version: 2007.01
-Revision: 1
-Depends: emacsen
-Recommends: mizar, mizar-gab
+Revision: 2
+Depends: emacsen, mizar
+Recommends: mizar-gab, mizar-mode-extras
Maintainer: Jesse Alama <[EMAIL PROTECTED]>
License: GPL
Homepage: http://wiki.mizar.org/cgi-bin/twiki/view/Mizar/MizarMode
@@ -32,10 +32,10 @@
(For more information on Mizar, see http://www.mizar.org)
The Emacs authoring environment for Mizar (MizarMode) is today the
-authoring tool of choice for many (probably majority of) Mizar
-authors.
+authoring tool of choice for many (probably the majority of) Mizar
+authors.
-Mizar is a non-programmable and non-tactical verifier, the proofs are
+Mizar is a non-programmable and non-tactical verifier; proofs are
developed in the traditional `write-compile-correct' software
programming loop. While this method is in the beginning more laborious
than the methods employed in tactical and programmable proof
@@ -43,9 +43,9 @@
maintainable and reusable. This seems to be a crucial factor for a
long-term and large-scale formalization effort.
-MizarMode has been designed with the aim to facilitate this kind of
-proof development by a number of `code-generating', `code-browsing'
-and `code-searching' methods or tools programmed or integrated within
+MizarMode has been designed to facilitate this kind of proof
+development by a number of `code-generating', `code-browsing' and
+`code-searching' methods or tools programmed or integrated within
it. These methods and tools now include e.g. the automated generation
of proof skeletons, proof advice using trained machine learning tools
like Mizar Proof Advisor or deductive tools like MoMM, semantic
@@ -68,6 +68,9 @@
(setq auto-mode-alist (append '( ("\\.miz" . mizar-mode)
("\\.abs" . mizar-mode))
auto-mode-alist))
+
+to your emacs initialization file. Add the form
+
(setq format-alist
(append '(
@@ -75,15 +78,19 @@
mmlquery-decode nil nil mmlquery-mode))
format-alist)
-to your emacs initialization file. In any case, the main entry point
-into the system is the command `mizar-mode'; type the key sequence
+if you would like to use the MML Query feature (for more information
+about MML query, see http://mmlquery.mizar.org).
+
+In any case, the main entry point into the system is the command
+`mizar-mode'; type the key sequence
M-x mizar-mode
to being structually editing Mizar code.
Finally, consider using the abbreviations defined in
-%p/share/doc/mizar-mode/abbrev_defs; they may help make entering Mizar
+%p/share/doc/mizar-mode/abbrev_defs; they may make editing Mizar
texts easier.
<<
+
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier.
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
Fink-commits mailing list
Fink-commits@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/fink-commits
