[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 MHonArc.