equal
deleted
inserted
replaced
126 \begin{matharray}{rcl} |
126 \begin{matharray}{rcl} |
127 @{command_def "fix"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
127 @{command_def "fix"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
128 @{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
128 @{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
129 @{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
129 @{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
130 @{command_def "define"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
130 @{command_def "define"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
131 @{command_def "def"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
|
132 \end{matharray} |
131 \end{matharray} |
133 |
132 |
134 The logical proof context consists of fixed variables and assumptions. The |
133 The logical proof context consists of fixed variables and assumptions. The |
135 former closely correspond to Skolem constants, or meta-level universal |
134 former closely correspond to Skolem constants, or meta-level universal |
136 quantification as provided by the Isabelle/Pure logical framework. |
135 quantification as provided by the Isabelle/Pure logical framework. |
167 ; |
166 ; |
168 prems: (@'if' (@{syntax props'} + @'and'))? |
167 prems: (@'if' (@{syntax props'} + @'and'))? |
169 ; |
168 ; |
170 @@{command define} @{syntax vars} @'where' |
169 @@{command define} @{syntax vars} @'where' |
171 (@{syntax props} + @'and') @{syntax for_fixes} |
170 (@{syntax props} + @'and') @{syntax for_fixes} |
172 ; |
|
173 @@{command def} (def + @'and') |
|
174 ; |
|
175 def: @{syntax thmdecl}? \<newline> |
|
176 @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}? |
|
177 \<close>} |
171 \<close>} |
178 |
172 |
179 \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary, |
173 \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary, |
180 but fixed\<close>. |
174 but fixed\<close>. |
181 |
175 |
205 definitions may be given as well, with a collective default name. |
199 definitions may be given as well, with a collective default name. |
206 |
200 |
207 \<^medskip> |
201 \<^medskip> |
208 It is also possible to abstract over local parameters as follows: \<^theory_text>\<open>define f |
202 It is also possible to abstract over local parameters as follows: \<^theory_text>\<open>define f |
209 :: "'a \<Rightarrow> 'b" where "f x = t" for x :: 'a\<close>. |
203 :: "'a \<Rightarrow> 'b" where "f x = t" for x :: 'a\<close>. |
210 |
|
211 \<^descr> \<^theory_text>\<open>def x \<equiv> t\<close> introduces a local (non-polymorphic) definition. This is an |
|
212 old form of \<^theory_text>\<open>define x where "x = t"\<close>. |
|
213 \<close> |
204 \<close> |
214 |
205 |
215 |
206 |
216 subsection \<open>Term abbreviations \label{sec:term-abbrev}\<close> |
207 subsection \<open>Term abbreviations \label{sec:term-abbrev}\<close> |
217 |
208 |