--- a/src/HOL/SetInterval.thy Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/SetInterval.thy Sat Sep 29 08:58:51 2007 +0200
@@ -17,19 +17,19 @@
begin
definition
lessThan :: "'a => 'a set" ("(1\<^loc>{..<_})") where
- "\<^loc>{..<u} == {x. x \<sqsubset> u}"
+ "\<^loc>{..<u} == {x. x \<^loc>< u}"
definition
atMost :: "'a => 'a set" ("(1\<^loc>{.._})") where
- "\<^loc>{..u} == {x. x \<sqsubseteq> u}"
+ "\<^loc>{..u} == {x. x \<^loc>\<le> u}"
definition
greaterThan :: "'a => 'a set" ("(1\<^loc>{_<..})") where
- "\<^loc>{l<..} == {x. l\<sqsubset>x}"
+ "\<^loc>{l<..} == {x. l\<^loc><x}"
definition
atLeast :: "'a => 'a set" ("(1\<^loc>{_..})") where
- "\<^loc>{l..} == {x. l\<sqsubseteq>x}"
+ "\<^loc>{l..} == {x. l\<^loc>\<le>x}"
definition
greaterThanLessThan :: "'a => 'a => 'a set" ("(1\<^loc>{_<..<_})") where