# HG changeset patch
# User haftmann
# Date 1171095974 -3600
# Node ID 5f8a2898668c1e0542ec13c8eb12d69799162d3f
# Parent  4d342f77fd74475bd6353288e591645a55d4ee6a
changed name of interpretation linorder to order

diff -r 4d342f77fd74 -r 5f8a2898668c src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Feb 10 09:26:12 2007 +0100
+++ b/src/HOL/Orderings.thy	Sat Feb 10 09:26:14 2007 +0100
@@ -876,14 +876,14 @@
   "linorder.max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = max"
   by (rule+) (simp add: max_def order.max_def)
 
-lemmas min_le_iff_disj = order.min_le_iff_disj [where 'b = "?'a::linorder", simplified min_linorder]
-lemmas le_max_iff_disj = order.le_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder]
-lemmas min_less_iff_disj = order.min_less_iff_disj [where 'b = "?'a::linorder", simplified min_linorder]
-lemmas less_max_iff_disj = order.less_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder]
-lemmas min_less_iff_conj [simp] = order.min_less_iff_conj [where 'b = "?'a::linorder", simplified min_linorder]
-lemmas max_less_iff_conj [simp] = order.max_less_iff_conj [where 'b = "?'a::linorder", simplified max_linorder]
-lemmas split_min = order.split_min [where 'b = "?'a::linorder", simplified min_linorder]
-lemmas split_max = order.split_max [where 'b = "?'a::linorder", simplified max_linorder]
+lemmas min_le_iff_disj = order.min_le_iff_disj [where 'b = "?'a::linorder", unfolded min_linorder]
+lemmas le_max_iff_disj = order.le_max_iff_disj [where 'b = "?'a::linorder", unfolded max_linorder]
+lemmas min_less_iff_disj = order.min_less_iff_disj [where 'b = "?'a::linorder", unfolded min_linorder]
+lemmas less_max_iff_disj = order.less_max_iff_disj [where 'b = "?'a::linorder", unfolded max_linorder]
+lemmas min_less_iff_conj [simp] = order.min_less_iff_conj [where 'b = "?'a::linorder", unfolded min_linorder]
+lemmas max_less_iff_conj [simp] = order.max_less_iff_conj [where 'b = "?'a::linorder", unfolded max_linorder]
+lemmas split_min = order.split_min [where 'b = "?'a::linorder", unfolded min_linorder]
+lemmas split_max = order.split_max [where 'b = "?'a::linorder", unfolded max_linorder]
 
 lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
   by (simp add: min_def)