equal
deleted
inserted
replaced
335 \begin{matharray}{rcll} |
335 \begin{matharray}{rcll} |
336 @{command_def "axiomatization"} & : & \<open>theory \<rightarrow> theory\<close> & (axiomatic!) \\ |
336 @{command_def "axiomatization"} & : & \<open>theory \<rightarrow> theory\<close> & (axiomatic!) \\ |
337 \end{matharray} |
337 \end{matharray} |
338 |
338 |
339 @{rail \<open> |
339 @{rail \<open> |
340 @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)? |
340 @@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)? |
341 ; |
341 ; |
342 specs: (@{syntax thmdecl}? @{syntax props} + @'and') |
342 axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and') |
|
343 prems @{syntax for_fixes} |
|
344 ; |
|
345 prems: (@'if' ((@{syntax prop}+) + @'and'))? |
343 \<close>} |
346 \<close>} |
344 |
347 |
345 \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants |
348 \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants |
346 simultaneously and states axiomatic properties for these. The constants are |
349 simultaneously and states axiomatic properties for these. The constants are |
347 marked as being specified once and for all, which prevents additional |
350 marked as being specified once and for all, which prevents additional |