tuned proofs;
authorwenzelm
Mon Jan 04 21:49:06 2016 +0100 (2016-01-04)
changeset 620531c8252d07e32
parent 62052 8bcbf1c93119
child 62054 cff7114e4572
tuned proofs;
src/HOL/Library/Product_Order.thy
     1.1 --- a/src/HOL/Library/Product_Order.thy	Mon Jan 04 21:42:32 2016 +0100
     1.2 +++ b/src/HOL/Library/Product_Order.thy	Mon Jan 04 21:49:06 2016 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4  instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
     1.5  
     1.6  instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
     1.7 -  by standard (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
     1.8 +  by standard (auto simp add: prod_eqI diff_eq)
     1.9  
    1.10  
    1.11  subsection \<open>Complete lattice operations\<close>
    1.12 @@ -179,7 +179,8 @@
    1.13  instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
    1.14      conditionally_complete_lattice
    1.15    by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
    1.16 -    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
    1.17 +    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq
    1.18 +    intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
    1.19  
    1.20  instance prod :: (complete_lattice, complete_lattice) complete_lattice
    1.21    by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def