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 63680 6e1e8b5abbfa
parent 62204 7f5579b12b0a
child 63884 d588f684ccaf
equal deleted inserted replaced
63679:dc311d55ad8f 63680:6e1e8b5abbfa 
    24 \<close>
 
    24 \<close>
 
    25 (*>*)
 
    25 (*>*)
 
    26 text\<open>
 
    26 text\<open>
 
    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>\<open>http://isabelle.in.tum.de/library/HOL\<close>.
 
    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