--- a/src/HOL/IsaMakefile Thu Mar 12 00:02:30 2009 +0100
+++ b/src/HOL/IsaMakefile Thu Mar 12 14:27:21 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
--- a/src/HOL/Library/OptionalSugar.thy Thu Mar 12 00:02:30 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy Thu Mar 12 14:27:21 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)