src/HOL/Lattices_Big.thy
changeset 61566 c3d6e570ccef
parent 61169 4de9ff3ea29a
child 61605 1bf7b186542e
     1.1 --- a/src/HOL/Lattices_Big.thy	Wed Nov 04 08:13:49 2015 +0100
     1.2 +++ b/src/HOL/Lattices_Big.thy	Wed Nov 04 08:13:52 2015 +0100
     1.3 @@ -319,7 +319,7 @@
     1.4    "Inf_fin = semilattice_set.F inf"
     1.5  
     1.6  sublocale Inf_fin!: semilattice_order_set inf less_eq less
     1.7 -where
     1.8 +rewrites
     1.9    "semilattice_set.F inf = Inf_fin"
    1.10  proof -
    1.11    show "semilattice_order_set inf less_eq less" ..
    1.12 @@ -337,7 +337,7 @@
    1.13    "Sup_fin = semilattice_set.F sup"
    1.14  
    1.15  sublocale Sup_fin!: semilattice_order_set sup greater_eq greater
    1.16 -where
    1.17 +rewrites
    1.18    "semilattice_set.F sup = Sup_fin"
    1.19  proof -
    1.20    show "semilattice_order_set sup greater_eq greater" ..
    1.21 @@ -492,7 +492,7 @@
    1.22  
    1.23  sublocale Min!: semilattice_order_set min less_eq less
    1.24    + Max!: semilattice_order_set max greater_eq greater
    1.25 -where
    1.26 +rewrites
    1.27    "semilattice_set.F min = Min"
    1.28    and "semilattice_set.F max = Max"
    1.29  proof -