doc-src/Locales/Locales/Examples3.thy
changeset 35423 6ef9525a5727
parent 33867 52643d0f856d
child 37206 7f2a6f3143ad
equal deleted 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" .