src/HOL/Library/Product_Order.thy
changeset 61166 5976fe402824
parent 60679 ade12ef2773c
child 62053 1c8252d07e32
     1.1 --- a/src/HOL/Library/Product_Order.thy	Sun Sep 13 16:50:12 2015 +0200
     1.2 +++ b/src/HOL/Library/Product_Order.thy	Sun Sep 13 20:20:16 2015 +0200
     1.3 @@ -233,7 +233,7 @@
     1.4  (* Contribution: Alessandro Coglio *)
     1.5  
     1.6  instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
     1.7 -proof (standard, goals)
     1.8 +proof (standard, goal_cases)
     1.9    case 1
    1.10    then show ?case
    1.11      by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)