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.
doc-src/Main/Docs/Main_Doc.thy
changeset 47870 ec815d64573f
parent 47682 8e2e87a0a594
equal deleted inserted replaced
47869:fa59eb662e6c 47870:ec815d64573f 
    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. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/dist/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. 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