equal
deleted
inserted
replaced
76 \mbox{\noquotes{@{prop[source] "m < (n::nat)"}}}. Type constraints may be |
76 \mbox{\noquotes{@{prop[source] "m < (n::nat)"}}}. Type constraints may be |
77 needed to |
77 needed to |
78 disambiguate terms involving overloaded functions such as @{text "+"}, @{text |
78 disambiguate terms involving overloaded functions such as @{text "+"}, @{text |
79 "*"} and @{text"\<le>"}. |
79 "*"} and @{text"\<le>"}. |
80 |
80 |
81 Finally there are the universal quantifier @{text"\<And>"} and the implication |
81 Finally there are the universal quantifier @{text"\<And>"}\index{$4@\isasymAnd} and the implication |
82 @{text"\<Longrightarrow>"}. They are part of the Isabelle framework, not the logic |
82 @{text"\<Longrightarrow>"}\index{$3@\isasymLongrightarrow}. They are part of the Isabelle framework, not the logic |
83 HOL. Logically, they agree with their HOL counterparts @{text"\<forall>"} and |
83 HOL. Logically, they agree with their HOL counterparts @{text"\<forall>"} and |
84 @{text"\<longrightarrow>"}, but operationally they behave differently. This will become |
84 @{text"\<longrightarrow>"}, but operationally they behave differently. This will become |
85 clearer as we go along. |
85 clearer as we go along. |
86 \begin{warn} |
86 \begin{warn} |
87 Right-arrows of all kinds always associate to the right. In particular, |
87 Right-arrows of all kinds always associate to the right. In particular, |
101 Roughly speaking, a \concept{theory} is a named collection of types, |
101 Roughly speaking, a \concept{theory} is a named collection of types, |
102 functions, and theorems, much like a module in a programming language. |
102 functions, and theorems, much like a module in a programming language. |
103 All the Isabelle text that you ever type needs to go into a theory. |
103 All the Isabelle text that you ever type needs to go into a theory. |
104 The general format of a theory @{text T} is |
104 The general format of a theory @{text T} is |
105 \begin{quote} |
105 \begin{quote} |
106 \isacom{theory} @{text T}\\ |
106 \indexed{\isacom{theory}}{theory} @{text T}\\ |
107 \isacom{imports} @{text "T\<^sub>1 \<dots> T\<^sub>n"}\\ |
107 \indexed{\isacom{imports}}{imports} @{text "T\<^sub>1 \<dots> T\<^sub>n"}\\ |
108 \isacom{begin}\\ |
108 \isacom{begin}\\ |
109 \emph{definitions, theorems and proofs}\\ |
109 \emph{definitions, theorems and proofs}\\ |
110 \isacom{end} |
110 \isacom{end} |
111 \end{quote} |
111 \end{quote} |
112 where @{text "T\<^sub>1 \<dots> T\<^sub>n"} are the names of existing |
112 where @{text "T\<^sub>1 \<dots> T\<^sub>n"} are the names of existing |