--- a/doc-src/Locales/Locales/Examples3.thy Tue Jul 07 17:39:51 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy Wed Jul 08 06:42:35 2009 +0200
@@ -152,7 +152,7 @@
apply (rule_tac x = "gcd x y" in exI)
apply auto [1]
apply (rule_tac x = "lcm x y" in exI)
- apply (auto intro: nat_lcm_least)
+ apply (auto intro: lcm_least_nat)
done
then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
@@ -168,7 +168,7 @@
apply (unfold nat_dvd.join_def)
apply (rule the_equality)
apply (unfold nat_dvd.is_sup_def)
- apply (auto intro: nat_lcm_least iff: nat_lcm_unique)
+ apply (auto intro: lcm_least_nat iff: lcm_unique_nat)
done
qed
--- a/doc-src/Locales/Locales/document/Examples3.tex Tue Jul 07 17:39:51 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex Wed Jul 08 06:42:35 2009 +0200
@@ -330,7 +330,7 @@
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}lcm\ x\ y{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}auto\ intro{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}least{\isacharparenright}\isanewline
+\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}least{\isacharunderscore}nat{\isacharparenright}\isanewline
\ \ \ \ \isacommand{done}\isamarkupfalse%
\isanewline
\ \ \isacommand{then}\isamarkupfalse%
@@ -364,7 +364,7 @@
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}auto\ intro{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}least\ iff{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}unique{\isacharparenright}\isanewline
+\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}least{\isacharunderscore}nat\ iff{\isacharcolon}\ lcm{\isacharunderscore}unique{\isacharunderscore}nat{\isacharparenright}\isanewline
\ \ \ \ \isacommand{done}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%