[isabelle] Floor and ceiling
I am using Isabelle 2013-2. I was trying to use the floor symbols
from the Symbols window. Looking at \<lfloor> under Punctuation, I
see abbrev: [. Looking at \<rfloor>, I see abbrev: .] So the floor of
x, then, should be [. x .] But then I looked at the ceiling symbols.
Looking at \<lceil>, I see abbrev: [. Looking at \<rceil>, I see
abbrev: .] So the ceiling of x, then, should also be [. x .] This
can't be right. What is [. x .] ? Is it floor(x) or is it ceiling(x)?
Or has this already been fixed in the 2014 edition? Thanks! -Douglas
Prof. W. Douglas Maurer Washington, DC 20052, USA
Department of Computer Science Tel. (1-202)994-5921
The George Washington University Fax (1-202)994-4875
This archive was generated by a fusion of
Pipermail (Mailman edition) and