# HG changeset patch
# User haftmann
# Date 1265634408 -3600
# Node ID 2c159d2cdae7787bc83fca9aba44340b747e504b
# Parent  8103ea95b1426daeb7fc35b59678f02b43fabade
dropped instantiations for combined lattices

diff -r 8103ea95b142 -r 2c159d2cdae7 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Mon Feb 08 14:06:46 2010 +0100
+++ b/src/HOL/NSA/StarDef.thy	Mon Feb 08 14:06:48 2010 +0100
@@ -849,12 +849,7 @@
     simp add: abs_ge_self abs_leI abs_triangle_ineq)+
 
 instance star :: (linordered_cancel_ab_semigroup_add) linordered_cancel_ab_semigroup_add ..
-instance star :: (semilattice_inf_ab_group_add) semilattice_inf_ab_group_add ..
-instance star :: (semilattice_inf_ab_group_add) semilattice_inf_ab_group_add ..
-instance star :: (lattice_ab_group_add) lattice_ab_group_add ..
 
-instance star :: (lattice_ab_group_add_abs) lattice_ab_group_add_abs
-by (intro_classes, transfer, rule abs_lattice)
 
 subsection {* Ring and field classes *}
 
@@ -934,7 +929,6 @@
 instance star :: (ordered_ring) ordered_ring ..
 instance star :: (ordered_ring_abs) ordered_ring_abs
   by intro_classes  (transfer, rule abs_eq_mult)
-instance star :: (lattice_ring) lattice_ring ..
 
 instance star :: (abs_if) abs_if
 by (intro_classes, transfer, rule abs_if)