1.1 --- a/src/HOL/IsaMakefile	Thu Mar 12 00:02:30 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Mar 12 14:27:21 2009 +0100
     1.3 @@ -344,7 +344,8 @@
     1.4    Library/Product_plus.thy \
     1.5    Library/Product_Vector.thy \
     1.6    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
     1.7 -  Library/reify_data.ML Library/reflection.ML
     1.8 +  Library/reify_data.ML Library/reflection.ML \
     1.9 +  Library/LaTeXsugar.thy Library/OptionalSugar.thy
    1.10  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    1.11  
    1.12  

     2.1 --- a/src/HOL/Library/OptionalSugar.thy	Thu Mar 12 00:02:30 2009 +0100
     2.2 +++ b/src/HOL/Library/OptionalSugar.thy	Thu Mar 12 14:27:21 2009 +0100
     2.3 @@ -4,13 +4,21 @@
     2.4  *)
     2.5  (*<*)
     2.6  theory OptionalSugar
     2.7 -imports LaTeXsugar
     2.8 +imports LaTeXsugar Complex_Main
     2.9  begin
    2.10  
    2.11 -(* set *)
    2.12 +(* hiding set *)
    2.13  translations
    2.14    "xs" <= "CONST set xs"
    2.15  
    2.16 +(* hiding numeric conversions - embeddings only *)
    2.17 +translations
    2.18 +  "n" <= "CONST of_nat n"
    2.19 +  "n" <= "CONST int n"
    2.20 +  "n" <= "real n"
    2.21 +  "n" <= "CONST real_of_nat n"
    2.22 +  "n" <= "CONST real_of_int n"
    2.23 +
    2.24  (* append *)
    2.25  syntax (latex output)
    2.26    "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)