# HG changeset patch
# User wenzelm
# Date 1236869792 -3600
# Node ID b0ce15e4633d4131b1a9147ac7e4adeb9f7c970b
# Parent  5e9248e8e2f8c67ffe1e2a5ec83808b34bf5d210# Parent  e0b66c11e7e4ef70655568f06504ddc91f9daa78
merged

diff -r e0b66c11e7e4 -r b0ce15e4633d src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Mar 12 15:54:58 2009 +0100
+++ b/src/HOL/Divides.thy	Thu Mar 12 15:56:32 2009 +0100
@@ -295,6 +295,27 @@
 
 end
 
+lemma div_mult_div_if_dvd: "(y::'a::{semiring_div,no_zero_divisors}) dvd x \<Longrightarrow> 
+  z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
+unfolding dvd_def
+  apply clarify
+  apply (case_tac "y = 0")
+  apply simp
+  apply (case_tac "z = 0")
+  apply simp
+  apply (simp add: algebra_simps)
+  apply (subst mult_assoc [symmetric])
+  apply (simp add: no_zero_divisors)
+done
+
+
+lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow>
+    (x div y)^n = x^n div y^n"
+apply (induct n)
+ apply simp
+apply(simp add: div_mult_div_if_dvd dvd_power_same)
+done
+
 class ring_div = semiring_div + comm_ring_1
 begin
 
diff -r e0b66c11e7e4 -r b0ce15e4633d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Mar 12 15:54:58 2009 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 12 15:56:32 2009 +0100
@@ -344,7 +344,8 @@
   Library/Product_plus.thy \
   Library/Product_Vector.thy \
   Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
-  Library/reify_data.ML Library/reflection.ML
+  Library/reify_data.ML Library/reflection.ML \
+  Library/LaTeXsugar.thy Library/OptionalSugar.thy
 	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
 
 
diff -r e0b66c11e7e4 -r b0ce15e4633d src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Thu Mar 12 15:54:58 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Thu Mar 12 15:56:32 2009 +0100
@@ -4,13 +4,21 @@
 *)
 (*<*)
 theory OptionalSugar
-imports LaTeXsugar
+imports LaTeXsugar Complex_Main
 begin
 
-(* set *)
+(* hiding set *)
 translations
   "xs" <= "CONST set xs"
 
+(* hiding numeric conversions - embeddings only *)
+translations
+  "n" <= "CONST of_nat n"
+  "n" <= "CONST int n"
+  "n" <= "real n"
+  "n" <= "CONST real_of_nat n"
+  "n" <= "CONST real_of_int n"
+
 (* append *)
 syntax (latex output)
   "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)