# HG changeset patch
# User nipkow
# Date 1247028210 -7200
# Node ID 683b5e3b31fc0591f85c772da6b0cd8c3e688d7a
# Parent  3fc19d2f0ac9e3d731c0cee149ba8d08997fd9c5# Parent  1984af09eb41aba545f74ed628739a021964e86b
merged

diff -r 3fc19d2f0ac9 -r 683b5e3b31fc doc-src/Locales/Locales/Examples3.thy
--- a/doc-src/Locales/Locales/Examples3.thy	Tue Jul 07 21:26:08 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy	Wed Jul 08 06:43:30 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
 
diff -r 3fc19d2f0ac9 -r 683b5e3b31fc doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Tue Jul 07 21:26:08 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Wed Jul 08 06:43:30 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%