src/HOL/Library/Product_Order.thy
changeset 60580 7e741e22d7fc
parent 60500 903bb1495239
child 60679 ade12ef2773c
     1.1 --- a/src/HOL/Library/Product_Order.thy	Thu Jun 25 22:56:33 2015 +0200
     1.2 +++ b/src/HOL/Library/Product_Order.thy	Thu Jun 25 23:33:47 2015 +0200
     1.3 @@ -233,11 +233,13 @@
     1.4  
     1.5  instance prod ::
     1.6    (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
     1.7 -proof
     1.8 -  case goal1 thus ?case
     1.9 +proof (default, goals)
    1.10 +  case 1
    1.11 +  then show ?case
    1.12      by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
    1.13  next
    1.14 -  case goal2 thus ?case
    1.15 +  case 2
    1.16 +  then show ?case
    1.17      by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
    1.18  qed
    1.19