]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/help/C/cicbrowser.html
Ignore *-stamp in matita/help/C
[helm.git] / matita / matita / help / C / cicbrowser.html
1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Browsing and searching</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets Vsnapshot" /><link rel="home" href="index.html" title="Matita V0.99.5 User Manual (rev. 0.99.5 )" /><link rel="up" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /><link rel="prev" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /><link rel="next" href="authoring.html" title="Authoring" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Browsing and searching</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_gettingstarted.html">Prev</a> </td><th width="60%" align="center">Chapter 3. Getting started</th><td width="20%" align="right"> <a accesskey="n" href="authoring.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="cicbrowser"></a>Browsing and searching</h2></div></div></div><p>The CIC browser is used to browse and search the library.
3     You can open a new CIC browser selecting "New Cic Browser"
4     from the "View" menu of Matita, or by pressing "F3".
5     The CIC browser is similar to a traditional Web browser.</p><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="browsinglib"></a>Browsing the library</h3></div></div></div><p>To browse the library, type in the location bar the absolute URI of
6     the theorem, definition or library fragment you are interested in.
7     "cic:/" is the root of the library. Contributions developed
8     in Matita are under "cic:/matita"; all the others are
9     part of the library of Coq.</p><p>Following the hyperlinks it is possible to navigate in the Web
10     of mathematical notions. Proof are rendered in pseudo-natural language
11     and mathematical notation is used for formulae. For now, mathematical
12     notation must be included in the current script to be activated, but we
13     plan to remove this limitation.</p></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="aboutproof"></a>Looking at a proof under development</h3></div></div></div><p>A proof under development is not yet part of the library.
14      The special URI "about:proof" can be used to browse the
15      proof currently under development, if there is one.
16      The "home" button of the CIC browser sets the location bar to
17      "about:proof".
18     </p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_gettingstarted.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_gettingstarted.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="authoring.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 3. Getting started </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Authoring</td></tr></table></div></body></html>