src/HOL/Orderings.thy
changeset 19931 fb32b43e7f80
parent 19656 09be06943252
child 19984 29bb4659f80a
     1.1 --- a/src/HOL/Orderings.thy	Tue Jun 20 14:51:59 2006 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Jun 20 15:53:44 2006 +0200
     1.3 @@ -388,7 +388,7 @@
     1.4  
     1.5  interpretation min_max:
     1.6    lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
     1.7 -apply(rule lower_semilattice_axioms.intro)
     1.8 +apply intro_locales
     1.9  apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.10  apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.11  apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.12 @@ -396,8 +396,7 @@
    1.13  
    1.14  interpretation min_max:
    1.15    upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
    1.16 -apply -
    1.17 -apply(rule upper_semilattice_axioms.intro)
    1.18 +apply intro_locales
    1.19  apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.20  apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.21  apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.22 @@ -405,11 +404,11 @@
    1.23  
    1.24  interpretation min_max:
    1.25    lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
    1.26 -.
    1.27 +  by intro_locales
    1.28  
    1.29  interpretation min_max:
    1.30    distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
    1.31 -apply(rule distrib_lattice_axioms.intro)
    1.32 +apply intro_locales
    1.33  apply(rule_tac x=x and y=y in linorder_le_cases)
    1.34  apply(rule_tac x=x and y=z in linorder_le_cases)
    1.35  apply(rule_tac x=y and y=z in linorder_le_cases)