equal
deleted
inserted
replaced
16 \<close> |
16 \<close> |
17 (*>*) |
17 (*>*) |
18 text\<open> |
18 text\<open> |
19 |
19 |
20 \begin{abstract} |
20 \begin{abstract} |
21 This document lists the main types, functions and syntax provided by theory \<^theory>\<open>Main\<close>. 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>https://isabelle.in.tum.de/library/HOL\<close>. |
21 This document lists the main types, functions and syntax provided by theory \<^theory>\<open>Main\<close>. 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>https://isabelle.in.tum.de/library/HOL/HOL\<close>. |
22 \end{abstract} |
22 \end{abstract} |
23 |
23 |
24 \section*{HOL} |
24 \section*{HOL} |
25 |
25 |
26 The basic logic: \<^prop>\<open>x = y\<close>, \<^const>\<open>True\<close>, \<^const>\<open>False\<close>, \<^prop>\<open>\<not> P\<close>, \<^prop>\<open>P \<and> Q\<close>, |
26 The basic logic: \<^prop>\<open>x = y\<close>, \<^const>\<open>True\<close>, \<^const>\<open>False\<close>, \<^prop>\<open>\<not> P\<close>, \<^prop>\<open>P \<and> Q\<close>, |