# HG changeset patch
# User nipkow
# Date 1236864455 -3600
# Node ID 03765a88f652ef297562bbe2f29a6b8e510f4647
# Parent  de9e8f1d927c673ed1e84b49aebbae08ee7be526# Parent  52e92009aacb0b6bf863e7b5a9063431070fbcd4
merged

diff -r de9e8f1d927c -r 03765a88f652 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Mar 12 13:18:42 2009 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 12 14:27:35 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 de9e8f1d927c -r 03765a88f652 src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Thu Mar 12 13:18:42 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Thu Mar 12 14:27:35 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)