products/Sources/formale Sprachen/Coq/clib/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: fixed_points.pvs   Sprache: PVS

rahmenlose Ansicht.lyx DruckansichtLatech {Latech[65] Isabelle[173] Fortran[198]}Entwicklung

#This file was created by <mike> Thu Dec 24 11:44:42 1998
#LyX 1.0 (C) 1995-1998 Matthias Ettrich and the LyX Team
\lyxformat 2.15
\textclass article
\language default
\inputencoding default
\fontscheme default
\graphics default
\paperfontsize default
\spacing single 
\papersize letterpaper
\paperpackage a4
\use_geometry 0
\use_amsmath 0
\paperorientation portrait
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\defskip medskip
\quotes_language english
\quotes_times 2
\papercolumns 1
\papersides 1
\paperpagestyle default

\layout Title

Introduction to LyX
\newline 
or
\newline 
How to Use These Doc Files!
\layout Author

by John Weiss and the LyX Team
\layout Section

Navigating the Documentation
\layout Standard

Welcome to LyX!
\layout Standard

To make it easier to answer your questions and describe all of the features
 of LyX, the documentation has been split up into several different files.
 Each one has its own purpose, as described below.
 Before you go plowing into any of those files, however, you should read
 this one thoroughly first, since it contains a lot of useful information
 and commentary that can save you some time.
\layout Standard
\added_space_top bigskip \align center 
WARNING!!!!! WARNING!!!!! WARNING!!!!
\layout Standard
\added_space_bottom bigskip \align center 
Danger, Will Robinson, Danger!
\layout Standard

Although LyX now has a version number of 1.0 [or greater], some of the documentat
ion may be incomplete or a version out of date.
 Like the rest of LyX, the manuals are the work of a group of volunteers
 who have 
\begin_inset Quotes eld
\end_inset 

Real Jobs,
\begin_inset Quotes erd
\end_inset 

 families, dishes to clean, kitty litter to dispose of, et cetera, et cetera,
 et cetera.
 We do our best to keep the manuals in tip-top shape, but we might not always
 succeed.
 [If you want to help remedy that situation, be sure to read section
\protected_separator 

\begin_inset LatexCommand \ref{sec:Contrib}

\end_inset 

 in addition to the rest of this document.]
\layout Standard

Also, please do us a favor---if anything in these manuals confuses you,
 is unclear, or wrong, don't hesitate to let us know! You can reach the
 current document maintainers by mailing to
\family typewriter 
 [email protected]
\family default 
.
\layout Section

The Format of the Manuals
\layout Standard

Some of you may have printed out the manual[s].
 Others may be reading it online, within LyX as a file.
 For those reading online, there are some differences from the printed version.
 First, the title is simply at the top of the document, not formatted on
 a separate page as in some of the printed versions.
 Nor are any of the footnotes or the Table of Contents visible.
 There is a popup for viewing the Table of Contents\SpecialChar \@.
 To open it, select 
\family sans 
Table
\protected_separator 
of
\protected_separator 
Contents
\family default 
 from the 
\family sans 
Edit
\family default 
 menu.
 To open a footnote, which looks like this,
\begin_float footnote 
\layout Standard

Hi!
\end_float 
 click on it with the left mouse button.
\layout Standard

Now that we've cleared up some of the differences between the printed and
 online versions of this file, we can start looking at the format of this
 document.
 You'll occasionally notice things in different fonts:
\layout Itemize


\emph on 
Emphasized Style
\emph default 
 is used for general emphasis, generic arguments, book titles, names of
 sections of other manuals, and notes from the authors.
\layout Itemize


\family typewriter 
Typewriter
\family default 
 is used for program and file names, LaTeX code, and LyX code and functions.
\layout Itemize


\family sans 
Sans Serif
\family default 
 is used for menu, button, or popup names, and the names of keyboard keys.
\layout Itemize


\noun on 
Noun Style
\noun default 
 is used for people's names.
\layout Standard

For keys and keybindings, you'll probably get referred to the
\emph on 
Key Bindings
\emph default 
 section of the 
\begin_inset Quotes eld
\end_inset 


\emph on 
Reference Manual
\emph default 

\begin_inset Quotes erd
\end_inset 

 [the file 
\family typewriter 
Reference.lyx
\family default 
].
 When we do need to reference keys, we'll use the following prefixing convention
:
\layout Itemize


\begin_inset Quotes eld
\end_inset 


\family sans 
C-
\family default 

\begin_inset Quotes eld
\end_inset 

 indicates the 
\family sans 
Control-
\family default 
 key.
\layout Itemize


\begin_inset Quotes eld
\end_inset 


\family sans 
S-
\family default 

\begin_inset Quotes eld
\end_inset 

 indicates the 
\family sans 
Shift-
\family default 
 key.
\layout Itemize


\begin_inset Quotes eld
\end_inset 


\family sans 
M-
\family default 

\begin_inset Quotes eld
\end_inset 

 indicates the 
\family sans 
Meta-
\family default 
 key, which on some keyboards will be the 
\family sans 
Alt-
\family default 
 key.
\layout Itemize


\begin_inset Quotes eld
\end_inset 


\family sans 
F1
\family default 

\begin_inset Quotes erd
\end_inset 

 \SpecialChar \ldots{}
 
\begin_inset Quotes eld
\end_inset 


\family sans 
F12
\family default 

\begin_inset Quotes erd
\end_inset 

 are the function keys.
\layout Itemize


\begin_inset Quotes eld
\end_inset 


\family sans 
Esc
\family default 

\begin_inset Quotes erd
\end_inset 

 is the escape key.
\layout Itemize


\begin_inset Quotes eld
\end_inset 


\family sans 
Left
\family default 

\begin_inset Quotes erd
\end_inset 

 
\begin_inset Quotes eld
\end_inset 


\family sans 
Right
\family default 

\begin_inset Quotes erd
\end_inset 

 
\begin_inset Quotes eld
\end_inset 


\family sans 
Up
\family default 

\begin_inset Quotes erd
\end_inset 

 
\begin_inset Quotes eld
\end_inset 


\family sans 
Down
\family default 

\begin_inset Quotes erd
\end_inset 

: self-explanatory.
\layout Itemize


\family sans 

\begin_inset Quotes eld
\end_inset 

Insert
\family default 

\begin_inset Quotes erd
\end_inset 

 
\begin_inset Quotes eld
\end_inset 


\family sans 
Delete
\family default 

\begin_inset Quotes erd
\end_inset 

 
\begin_inset Quotes eld
\end_inset 


\family sans 
Home
\family default 

\begin_inset Quotes erd
\end_inset 

 
\begin_inset Quotes eld
\end_inset 


\family sans 
End
\family default 

\begin_inset Quotes erd
\end_inset 

 
\begin_inset Quotes eld
\end_inset 


\family sans 
PageUp
\family default 

\begin_inset Quotes erd
\end_inset 

 
\begin_inset Quotes eld
\end_inset 


\family sans 
PageDown
\family default 

\begin_inset Quotes erd
\end_inset 

: these are the 6 keys that appear above the cursor keys on many PC keyboards.
 
\begin_inset Quotes eld
\end_inset 


\family sans 
PageUp
\family default 

\begin_inset Quotes erd
\end_inset 

 and 
\begin_inset Quotes eld
\end_inset 


\family sans 
PageDown
\family default 

\begin_inset Quotes erd
\end_inset 

 are called 
\begin_inset Quotes eld
\end_inset 


\family sans 
Prior
\family default 

\begin_inset Quotes erd
\end_inset 

 and 
\begin_inset Quotes eld
\end_inset 


\family sans 
Next
\family default 

\begin_inset Quotes erd
\end_inset 

 on some keyboards.
\layout Itemize


\family sans 
Return
\family default 
 and 
\family sans 
Enter
\family default 
 both refer to the same key.
 Some keyboards label the 
\family sans 
Return
\family default 
 key as 
\begin_inset Quotes eld
\end_inset 

Return,
\begin_inset Quotes erd
\end_inset 

 others as 
\begin_inset Quotes eld
\end_inset 

Enter,
\begin_inset Quotes erd
\end_inset 

 still others have two keys.
 LyX treats all of them as the same key, so we'll use
\family sans 
Return
\family default 
 and 
\family sans 
Enter
\family default 
 interchangeably.
\layout Standard

You'll also see something like
\begin_inset Quotes eld
\end_inset 

[See the 
\emph on 

\begin_inset Quotes els
\end_inset 

Reference Manual
\emph default 

\begin_inset Quotes ers
\end_inset 

]
\begin_inset Quotes erd
\end_inset 

 from time to time.
 We've listed the possible default keybindings for a function in its entry
 in the 
\begin_inset Quotes eld
\end_inset 


\emph on 
Reference Manual
\emph default 
,
\begin_inset Quotes erd
\end_inset 

 so check there, too.
\layout Section

The Manuals
\layout Standard

The following list describes the contents of each of the files in the documentat
ion:
\layout Description


\emph on 
Introduction 
\protected_separator 

\emph default 

\newline 
This file.
\layout Description


\emph on 
Tutorial 
\protected_separator 

\emph default 

\newline 
If you are new to LyX, and never used LaTeX before, or never even heard
 of LaTeX, then you should start here.
 If you 
\emph on 
have
\emph default 
 used LaTeX before, you should still read the section on 
\begin_inset Quotes eld
\end_inset 

LyX for LaTeX users
\begin_inset Quotes erd
\end_inset 

 [and skimming the rest of the document wouldn't hurt].
\layout Description


\emph on 
User's
\protected_separator 
Guide 
\protected_separator 

\emph default 

\newline 
The primary documentation.
 We'll attempt to cover
\emph on 
most
\emph default 
 of the basic operation and available features of LyX here.
 The main manual assumes that you have a passing knowledge of LaTeX, or
 that you've read the
\emph on 
Tutorial
\emph default 
\latex latex 
\SpecialChar \@.

\layout Description


\emph on 
Extended
\protected_separator 
Features 
\protected_separator 

\newline 

\emph default 
Extension of the 
\emph on 
User's Guide
\emph default 
.
 Documents additional layouts and special-purpose editing features, including
 some of the tricks of the LaTeX masters.
\layout Description


\emph on 
Customization 
\protected_separator 

\emph default 

\newline 
A description of advanced LyX features, including how to customize the overall
 behavior of LyX\SpecialChar \@.
 This includes such things as keybindings, internationalization,
 and configuration files.
\layout Description


\emph on 
Reference
\protected_separator 
Manual 
\protected_separator 

\emph default 

\newline 
This contains an exhaustive, detailed description of the features of LyX,
 but without the helpful usage hints and descriptions found in the 
\emph on 
User's Guide
\emph default 
 or other manuals.
\layout Description


\emph on 
Known
\protected_separator 
bugs 
\protected_separator 

\emph default 

\newline 
This file contains a list of known bugs in LyX, and also information on
 what you should do if you find a bug in LyX\SpecialChar \@.

\layout Description


\emph on 
LaTeX
\protected_separator 
configuration 
\protected_separator 

\emph default 

\newline 
LyX investigates your system upon installation.
 This file contains info on what LyX learned about your installation.
 Check it to see if you're missing something you might like to have.
\layout Standard

These files will reference one another as necessary.
 For example, the 
\emph on 
User's Guide
\emph default 
 contains 
\emph on 
some
\emph default 
 information on installation and customization, but refers the reader to
 the 
\emph on 
Customization Manual
\emph default 
 for more information.
\layout Standard

We'll state again an important point:
\layout Standard
\added_space_top 0.51cm \added_space_bottom 0.51cm \align center 
If you've never used or even heard of LaTeX before, read the
\emph on 
Tutorial
\emph default 
.
 Now\SpecialChar \@.

\layout Standard

Otherwise, LyX will seem byzantine and unusable to you.
\layout Section


\begin_inset LatexCommand \label{sec:Contrib}

\end_inset 

Contributing to the Documentation Project
\layout Subsection

Reporting Errors in the Manuals
\layout Standard

That's easy enough to do.
 You could post a message to either the Developer's Mailing List or the
 User's Mailing List.
 The Documentation Team, however, would prefer you to send a message to
 
\family typewriter 
[email protected]
\family default 
.
 If the fixes are minor, someone will do them.
 If they're major, we suggest you join the mailing list and talk with us
 for a while before doing anything.
\layout Standard
\added_space_top 1.06cm \added_space_bottom 1.06cm \align center 

\emph on 
Never make changes to any of the manuals without prior consent of the Documentat
ion Team!
\layout Standard

Any such random changes won't make it into the documentation, anyways, since
 the Documentation Team maintains the master copies via the CVS tree.
\layout Subsection

Joining the Documentation Team.
\layout Standard

The LyX Documentation Project, like anything else in the LyX project, can
 always use assistance! If you're interested in contributing to the Documentatio
n Project, you need to do the following assignment 
\emph on 
first
\emph default 
:
\layout Enumerate

Get the latest LyX source code.
 Untar it.
 You will find a directory inside the main tree called 
\family typewriter 
development
\family default 
.
 Inside that directory is a file called 
\family typewriter 
DocStyle.lyx
\family default 
.
 Read it; it's the style sheet for the documentation.
\layout Enumerate

Take a break for a day or two, then go read 
\family typewriter 
DocStyle.lyx
\family default 
 again.
\layout Enumerate

Next, read the 
\emph on 
User's Guide
\emph default 
 and the 
\emph on 
Tutorial
\emph default 
.
 
\begin_deeper 
\layout Standard

The point of this exercise is to give you ideas.
 The 
\emph on 
Tutorial
\emph default 
 and 
\emph on 
User's Guide
\emph default 
 will always be the most up-to-date of all of the documentation.
 You should be able to glean some insights into how we want the manuals
 to read and to look.
\end_deeper 
\layout Enumerate

Read 
\family typewriter 
DocStyle.lyx
\family default 
 again.
\layout Enumerate

Lastly, contact the team at: 
\begin_deeper 
\layout Standard


\family typewriter 
[email protected]
\layout Standard

We want to make sure that you understand the style sheet 
\emph on 
before
\emph default 
 you start writing.
 Otherwise, we'll make you rewrite your submissions.
\end_deeper 
\layout Standard


\emph on 
Don't
\emph default 
even think about starting to write anything until we chat via email.
 You can review any current activity with the documents on the Documentation
 Team web page [once we get it up] or through the mailing list archives
 at 
\family typewriter 
www.lyx.org
\family default 
.
\the_end

[ Verzeichnis aufwärts0.104unsichere Verbindung  ]