Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Doc/Main/Main_Doc.thy
changeset 54703 499f92dc6e45
parent 53328 9228c575d67d
child 54744 1e7f2d296e19
equal deleted inserted replaced
54702:3daeba5130f0 54703:499f92dc6e45 
    24 *}
 
    24 *}
 
    25 (*>*)
 
    25 (*>*)
 
    26 text{*
 
    26 text{*
 
    27 
    27 
    28 \begin{abstract}
 
    28 \begin{abstract}
 
    29 This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/library/HOL/}.
 
    29 This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see @{url "http://isabelle.in.tum.de/library/HOL/"}.
 
    30 \end{abstract}
 
    30 \end{abstract}
 
    31 
    31 
    32 \section*{HOL}
 
    32 \section*{HOL}
 
    33 
    33 
    34 The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}.
 
    34 The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}.
isabelle