doc-src/Locales/Locales/Examples3.thy
 changeset 35423 6ef9525a5727 parent 33867 52643d0f856d child 37206 7f2a6f3143ad
equal inserted replaced
35422:e74b6f3b950c 35423:6ef9525a5727
`    61       apply (unfold int.is_inf_def int.is_sup_def)`
`    61       apply (unfold int.is_inf_def int.is_sup_def)`
`    62       txt {* \normalsize the goals are transformed to these`
`    62       txt {* \normalsize the goals are transformed to these`
`    63 	statements:`
`    63 	statements:`
`    64 	@{subgoals [display]}`
`    64 	@{subgoals [display]}`
`    65 	This is Presburger arithmetic, which can be solved by the`
`    65 	This is Presburger arithmetic, which can be solved by the`
`    66 	method @{text arith}. *}`
`    66         method @{text arith}. *}`
`    67       by arith+`
`    67       by arith+`
`    68     txt {* \normalsize In order to show the equations, we put ourselves`
`    68     txt {* \normalsize In order to show the equations, we put ourselves`
`    69       in a situation where the lattice theorems can be used in a`
`    69       in a situation where the lattice theorems can be used in a`
`    70       convenient way. *}`
`    70       convenient way. *}`
`    71     then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" .`
`    71     then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" .`