--- a/doc-src/Locales/Locales/Examples2.thy Thu Oct 15 22:07:18 2009 +0200
+++ b/doc-src/Locales/Locales/Examples2.thy Thu Oct 15 22:22:08 2009 +0200
@@ -2,16 +2,16 @@
imports Examples
begin
text {* \vspace{-5ex} *}
- interpretation %visible nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool"
- where "partial_order.less op \<le> (x::nat) y = (x < y)"
+ interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
+ where "partial_order.less op \<le> (x::int) y = (x < y)"
proof -
txt {* \normalsize The goals are @{subgoals [display]}
The proof that @{text \<le>} is a partial order is as above. *}
- show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+ show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
by unfold_locales auto
txt {* \normalsize The second goal is shown by unfolding the
definition of @{term "partial_order.less"}. *}
- show "partial_order.less op \<le> (x::nat) y = (x < y)"
+ show "partial_order.less op \<le> (x::int) y = (x < y)"
unfolding partial_order.less_def [OF `partial_order op \<le>`]
by auto
qed