src/HOL/Library/OptionalSugar.thy
changeset 30502 b80d2621caee
parent 30474 52e92009aacb
child 30503 201887dcea0a
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Thu Mar 12 23:12:53 2009 +0100
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Fri Mar 13 12:32:29 2009 +0100
     1.3 @@ -18,6 +18,8 @@
     1.4    "n" <= "real n"
     1.5    "n" <= "CONST real_of_nat n"
     1.6    "n" <= "CONST real_of_int n"
     1.7 +  "n" <= "CONST of_real n"
     1.8 +  "n" <= "CONST complex_of_real n"
     1.9  
    1.10  (* append *)
    1.11  syntax (latex output)