src/HOL/Orderings.thy
changeset 25062 af5ef0d4d655
parent 24920 2a45e400fdad
child 25076 a50b36401c61
     1.1 --- a/src/HOL/Orderings.thy	Tue Oct 16 23:12:38 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Oct 16 23:12:45 2007 +0200
     1.3 @@ -14,10 +14,10 @@
     1.4  subsection {* Partial orders *}
     1.5  
     1.6  class order = ord +
     1.7 -  assumes less_le: "x \<^loc>< y \<longleftrightarrow> x \<^loc>\<le> y \<and> x \<noteq> y"
     1.8 -  and order_refl [iff]: "x \<^loc>\<le> x"
     1.9 -  and order_trans: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> z"
    1.10 -  assumes antisym: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
    1.11 +  assumes less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
    1.12 +  and order_refl [iff]: "x \<le> x"
    1.13 +  and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
    1.14 +  assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
    1.15  
    1.16  begin
    1.17  
    1.18 @@ -28,94 +28,94 @@
    1.19  
    1.20  text {* Reflexivity. *}
    1.21  
    1.22 -lemma eq_refl: "x = y \<Longrightarrow> x \<^loc>\<le> y"
    1.23 +lemma eq_refl: "x = y \<Longrightarrow> x \<le> y"
    1.24      -- {* This form is useful with the classical reasoner. *}
    1.25  by (erule ssubst) (rule order_refl)
    1.26  
    1.27 -lemma less_irrefl [iff]: "\<not> x \<^loc>< x"
    1.28 +lemma less_irrefl [iff]: "\<not> x < x"
    1.29  by (simp add: less_le)
    1.30  
    1.31 -lemma le_less: "x \<^loc>\<le> y \<longleftrightarrow> x \<^loc>< y \<or> x = y"
    1.32 +lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
    1.33      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
    1.34  by (simp add: less_le) blast
    1.35  
    1.36 -lemma le_imp_less_or_eq: "x \<^loc>\<le> y \<Longrightarrow> x \<^loc>< y \<or> x = y"
    1.37 +lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
    1.38  unfolding less_le by blast
    1.39  
    1.40 -lemma less_imp_le: "x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y"
    1.41 +lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
    1.42  unfolding less_le by blast
    1.43  
    1.44 -lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
    1.45 +lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
    1.46  by (erule contrapos_pn, erule subst, rule less_irrefl)
    1.47  
    1.48  
    1.49  text {* Useful for simplification, but too risky to include by default. *}
    1.50  
    1.51 -lemma less_imp_not_eq: "x \<^loc>< y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
    1.52 +lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
    1.53  by auto
    1.54  
    1.55 -lemma less_imp_not_eq2: "x \<^loc>< y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
    1.56 +lemma less_imp_not_eq2: "x < y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
    1.57  by auto
    1.58  
    1.59  
    1.60  text {* Transitivity rules for calculational reasoning *}
    1.61  
    1.62 -lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<^loc>\<le> b \<Longrightarrow> a \<^loc>< b"
    1.63 +lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
    1.64  by (simp add: less_le)
    1.65  
    1.66 -lemma le_neq_trans: "a \<^loc>\<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<^loc>< b"
    1.67 +lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b"
    1.68  by (simp add: less_le)
    1.69  
    1.70  
    1.71  text {* Asymmetry. *}
    1.72  
    1.73 -lemma less_not_sym: "x \<^loc>< y \<Longrightarrow> \<not> (y \<^loc>< x)"
    1.74 +lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"
    1.75  by (simp add: less_le antisym)
    1.76  
    1.77 -lemma less_asym: "x \<^loc>< y \<Longrightarrow> (\<not> P \<Longrightarrow> y \<^loc>< x) \<Longrightarrow> P"
    1.78 +lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P"
    1.79  by (drule less_not_sym, erule contrapos_np) simp
    1.80  
    1.81 -lemma eq_iff: "x = y \<longleftrightarrow> x \<^loc>\<le> y \<and> y \<^loc>\<le> x"
    1.82 +lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
    1.83  by (blast intro: antisym)
    1.84  
    1.85 -lemma antisym_conv: "y \<^loc>\<le> x \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
    1.86 +lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
    1.87  by (blast intro: antisym)
    1.88  
    1.89 -lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
    1.90 +lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
    1.91  by (erule contrapos_pn, erule subst, rule less_irrefl)
    1.92  
    1.93  
    1.94  text {* Transitivity. *}
    1.95  
    1.96 -lemma less_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
    1.97 +lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
    1.98  by (simp add: less_le) (blast intro: order_trans antisym)
    1.99  
   1.100 -lemma le_less_trans: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
   1.101 +lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
   1.102  by (simp add: less_le) (blast intro: order_trans antisym)
   1.103  
   1.104 -lemma less_le_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<^loc>< z"
   1.105 +lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
   1.106  by (simp add: less_le) (blast intro: order_trans antisym)
   1.107  
   1.108  
   1.109  text {* Useful for simplification, but too risky to include by default. *}
   1.110  
   1.111 -lemma less_imp_not_less: "x \<^loc>< y \<Longrightarrow> (\<not> y \<^loc>< x) \<longleftrightarrow> True"
   1.112 +lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True"
   1.113  by (blast elim: less_asym)
   1.114  
   1.115 -lemma less_imp_triv: "x \<^loc>< y \<Longrightarrow> (y \<^loc>< x \<longrightarrow> P) \<longleftrightarrow> True"
   1.116 +lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True"
   1.117  by (blast elim: less_asym)
   1.118  
   1.119  
   1.120  text {* Transitivity rules for calculational reasoning *}
   1.121  
   1.122 -lemma less_asym': "a \<^loc>< b \<Longrightarrow> b \<^loc>< a \<Longrightarrow> P"
   1.123 +lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P"
   1.124  by (rule less_asym)
   1.125  
   1.126  
   1.127  text {* Reverse order *}
   1.128  
   1.129  lemma order_reverse:
   1.130 -  "order (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
   1.131 +  "order (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
   1.132  by unfold_locales
   1.133     (simp add: less_le, auto intro: antisym order_trans)
   1.134  
   1.135 @@ -128,67 +128,67 @@
   1.136    assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
   1.137  begin
   1.138  
   1.139 -lemma less_linear: "x \<^loc>< y \<or> x = y \<or> y \<^loc>< x"
   1.140 +lemma less_linear: "x < y \<or> x = y \<or> y < x"
   1.141  unfolding less_le using less_le linear by blast
   1.142  
   1.143 -lemma le_less_linear: "x \<^loc>\<le> y \<or> y \<^loc>< x"
   1.144 +lemma le_less_linear: "x \<le> y \<or> y < x"
   1.145  by (simp add: le_less less_linear)
   1.146  
   1.147  lemma le_cases [case_names le ge]:
   1.148 -  "(x \<^loc>\<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>\<le> x \<Longrightarrow> P) \<Longrightarrow> P"
   1.149 +  "(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
   1.150  using linear by blast
   1.151  
   1.152  lemma linorder_cases [case_names less equal greater]:
   1.153 -  "(x \<^loc>< y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> P) \<Longrightarrow> P"
   1.154 +  "(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P"
   1.155  using less_linear by blast
   1.156  
   1.157 -lemma not_less: "\<not> x \<^loc>< y \<longleftrightarrow> y \<^loc>\<le> x"
   1.158 +lemma not_less: "\<not> x < y \<longleftrightarrow> y \<le> x"
   1.159  apply (simp add: less_le)
   1.160  using linear apply (blast intro: antisym)
   1.161  done
   1.162  
   1.163  lemma not_less_iff_gr_or_eq:
   1.164 - "\<not>(x \<^loc>< y) \<longleftrightarrow> (x \<^loc>> y | x = y)"
   1.165 + "\<not>(x < y) \<longleftrightarrow> (x > y | x = y)"
   1.166  apply(simp add:not_less le_less)
   1.167  apply blast
   1.168  done
   1.169  
   1.170 -lemma not_le: "\<not> x \<^loc>\<le> y \<longleftrightarrow> y \<^loc>< x"
   1.171 +lemma not_le: "\<not> x \<le> y \<longleftrightarrow> y < x"
   1.172  apply (simp add: less_le)
   1.173  using linear apply (blast intro: antisym)
   1.174  done
   1.175  
   1.176 -lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x \<^loc>< y \<or> y \<^loc>< x"
   1.177 +lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x < y \<or> y < x"
   1.178  by (cut_tac x = x and y = y in less_linear, auto)
   1.179  
   1.180 -lemma neqE: "x \<noteq> y \<Longrightarrow> (x \<^loc>< y \<Longrightarrow> R) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> R) \<Longrightarrow> R"
   1.181 +lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R"
   1.182  by (simp add: neq_iff) blast
   1.183  
   1.184 -lemma antisym_conv1: "\<not> x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
   1.185 +lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
   1.186  by (blast intro: antisym dest: not_less [THEN iffD1])
   1.187  
   1.188 -lemma antisym_conv2: "x \<^loc>\<le> y \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
   1.189 +lemma antisym_conv2: "x \<le> y \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
   1.190  by (blast intro: antisym dest: not_less [THEN iffD1])
   1.191  
   1.192 -lemma antisym_conv3: "\<not> y \<^loc>< x \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
   1.193 +lemma antisym_conv3: "\<not> y < x \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
   1.194  by (blast intro: antisym dest: not_less [THEN iffD1])
   1.195  
   1.196  text{*Replacing the old Nat.leI*}
   1.197 -lemma leI: "\<not> x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x"
   1.198 +lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x"
   1.199  unfolding not_less .
   1.200  
   1.201 -lemma leD: "y \<^loc>\<le> x \<Longrightarrow> \<not> x \<^loc>< y"
   1.202 +lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
   1.203  unfolding not_less .
   1.204  
   1.205  (*FIXME inappropriate name (or delete altogether)*)
   1.206 -lemma not_leE: "\<not> y \<^loc>\<le> x \<Longrightarrow> x \<^loc>< y"
   1.207 +lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y"
   1.208  unfolding not_le .
   1.209  
   1.210  
   1.211  text {* Reverse order *}
   1.212  
   1.213  lemma linorder_reverse:
   1.214 -  "linorder (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
   1.215 +  "linorder (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
   1.216  by unfold_locales
   1.217    (simp add: less_le, auto intro: antisym order_trans simp add: linear)
   1.218  
   1.219 @@ -199,42 +199,42 @@
   1.220  
   1.221  definition (in ord)
   1.222    min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.223 -  [code unfold, code inline del]: "min a b = (if a \<^loc>\<le> b then a else b)"
   1.224 +  [code unfold, code inline del]: "min a b = (if a \<le> b then a else b)"
   1.225  
   1.226  definition (in ord)
   1.227    max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.228 -  [code unfold, code inline del]: "max a b = (if a \<^loc>\<le> b then b else a)"
   1.229 +  [code unfold, code inline del]: "max a b = (if a \<le> b then b else a)"
   1.230  
   1.231  lemma min_le_iff_disj:
   1.232 -  "min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
   1.233 +  "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
   1.234  unfolding min_def using linear by (auto intro: order_trans)
   1.235  
   1.236  lemma le_max_iff_disj:
   1.237 -  "z \<^loc>\<le> max x y \<longleftrightarrow> z \<^loc>\<le> x \<or> z \<^loc>\<le> y"
   1.238 +  "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
   1.239  unfolding max_def using linear by (auto intro: order_trans)
   1.240  
   1.241  lemma min_less_iff_disj:
   1.242 -  "min x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<or> y \<^loc>< z"
   1.243 +  "min x y < z \<longleftrightarrow> x < z \<or> y < z"
   1.244  unfolding min_def le_less using less_linear by (auto intro: less_trans)
   1.245  
   1.246  lemma less_max_iff_disj:
   1.247 -  "z \<^loc>< max x y \<longleftrightarrow> z \<^loc>< x \<or> z \<^loc>< y"
   1.248 +  "z < max x y \<longleftrightarrow> z < x \<or> z < y"
   1.249  unfolding max_def le_less using less_linear by (auto intro: less_trans)
   1.250  
   1.251  lemma min_less_iff_conj [simp]:
   1.252 -  "z \<^loc>< min x y \<longleftrightarrow> z \<^loc>< x \<and> z \<^loc>< y"
   1.253 +  "z < min x y \<longleftrightarrow> z < x \<and> z < y"
   1.254  unfolding min_def le_less using less_linear by (auto intro: less_trans)
   1.255  
   1.256  lemma max_less_iff_conj [simp]:
   1.257 -  "max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z"
   1.258 +  "max x y < z \<longleftrightarrow> x < z \<and> y < z"
   1.259  unfolding max_def le_less using less_linear by (auto intro: less_trans)
   1.260  
   1.261  lemma split_min [noatp]:
   1.262 -  "P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)"
   1.263 +  "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
   1.264  by (simp add: min_def)
   1.265  
   1.266  lemma split_max [noatp]:
   1.267 -  "P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)"
   1.268 +  "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
   1.269  by (simp add: max_def)
   1.270  
   1.271  end
   1.272 @@ -371,109 +371,109 @@
   1.273  (* The type constraint on @{term op =} below is necessary since the operation
   1.274     is not a parameter of the locale. *)
   1.275  lemmas (in order)
   1.276 -  [order add less_reflE: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.277 +  [order add less_reflE: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.278    less_irrefl [THEN notE]
   1.279  lemmas (in order)
   1.280 -  [order add le_refl: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.281 +  [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.282    order_refl
   1.283  lemmas (in order)
   1.284 -  [order add less_imp_le: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.285 +  [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.286    less_imp_le
   1.287  lemmas (in order)
   1.288 -  [order add eqI: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.289 +  [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.290    antisym
   1.291  lemmas (in order)
   1.292 -  [order add eqD1: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.293 +  [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.294    eq_refl
   1.295  lemmas (in order)
   1.296 -  [order add eqD2: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.297 +  [order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.298    sym [THEN eq_refl]
   1.299  lemmas (in order)
   1.300 -  [order add less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.301 +  [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.302    less_trans
   1.303  lemmas (in order)
   1.304 -  [order add less_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.305 +  [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.306    less_le_trans
   1.307  lemmas (in order)
   1.308 -  [order add le_less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.309 +  [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.310    le_less_trans
   1.311  lemmas (in order)
   1.312 -  [order add le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.313 +  [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.314    order_trans
   1.315  lemmas (in order)
   1.316 -  [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.317 +  [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.318    le_neq_trans
   1.319  lemmas (in order)
   1.320 -  [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.321 +  [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.322    neq_le_trans
   1.323  lemmas (in order)
   1.324 -  [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.325 +  [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.326    less_imp_neq
   1.327  lemmas (in order)
   1.328 -  [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.329 +  [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.330     eq_neq_eq_imp_neq
   1.331  lemmas (in order)
   1.332 -  [order add not_sym: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.333 +  [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.334    not_sym
   1.335  
   1.336 -lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = _
   1.337 +lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _
   1.338  
   1.339  lemmas (in linorder)
   1.340 -  [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.341 +  [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.342    less_irrefl [THEN notE]
   1.343  lemmas (in linorder)
   1.344 -  [order add le_refl: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.345 +  [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.346    order_refl
   1.347  lemmas (in linorder)
   1.348 -  [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.349 +  [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.350    less_imp_le
   1.351  lemmas (in linorder)
   1.352 -  [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.353 +  [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.354    not_less [THEN iffD2]
   1.355  lemmas (in linorder)
   1.356 -  [order add not_leI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.357 +  [order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.358    not_le [THEN iffD2]
   1.359  lemmas (in linorder)
   1.360 -  [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.361 +  [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.362    not_less [THEN iffD1]
   1.363  lemmas (in linorder)
   1.364 -  [order add not_leD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.365 +  [order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.366    not_le [THEN iffD1]
   1.367  lemmas (in linorder)
   1.368 -  [order add eqI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.369 +  [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.370    antisym
   1.371  lemmas (in linorder)
   1.372 -  [order add eqD1: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.373 +  [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.374    eq_refl
   1.375  lemmas (in linorder)
   1.376 -  [order add eqD2: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.377 +  [order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.378    sym [THEN eq_refl]
   1.379  lemmas (in linorder)
   1.380 -  [order add less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.381 +  [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.382    less_trans
   1.383  lemmas (in linorder)
   1.384 -  [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.385 +  [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.386    less_le_trans
   1.387  lemmas (in linorder)
   1.388 -  [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.389 +  [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.390    le_less_trans
   1.391  lemmas (in linorder)
   1.392 -  [order add le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.393 +  [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.394    order_trans
   1.395  lemmas (in linorder)
   1.396 -  [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.397 +  [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.398    le_neq_trans
   1.399  lemmas (in linorder)
   1.400 -  [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.401 +  [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.402    neq_le_trans
   1.403  lemmas (in linorder)
   1.404 -  [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.405 +  [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.406    less_imp_neq
   1.407  lemmas (in linorder)
   1.408 -  [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.409 +  [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.410    eq_neq_eq_imp_neq
   1.411  lemmas (in linorder)
   1.412 -  [order add not_sym: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
   1.413 +  [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.414    not_sym
   1.415  
   1.416