equal
deleted
inserted
replaced
18 |
18 |
19 syntax (xsymbols) |
19 syntax (xsymbols) |
20 floor :: "real => int" ("\<lfloor>_\<rfloor>") |
20 floor :: "real => int" ("\<lfloor>_\<rfloor>") |
21 ceiling :: "real => int" ("\<lceil>_\<rceil>") |
21 ceiling :: "real => int" ("\<lceil>_\<rceil>") |
22 |
22 |
|
23 syntax (HTML output) |
|
24 floor :: "real => int" ("\<lfloor>_\<rfloor>") |
|
25 ceiling :: "real => int" ("\<lceil>_\<rceil>") |
23 |
26 |
24 |
27 |
25 lemma number_of_less_real_of_int_iff [simp]: |
28 lemma number_of_less_real_of_int_iff [simp]: |
26 "((number_of n) < real (m::int)) = (number_of n < m)" |
29 "((number_of n) < real (m::int)) = (number_of n < m)" |
27 apply auto |
30 apply auto |