src/HOL/AxClasses/Lattice/LatPreInsts.ML
changeset 5711 5a1cd4b4b20e
parent 5069 3ea049f7979d
equal deleted inserted replaced
5710:30f4d3713cbe 5711:5a1cd4b4b20e
     1 
       
     2 open LatPreInsts;
       
     3 
     1 
     4 
     2 
     5 (** complete lattices **)
     3 (** complete lattices **)
     6 
     4 
     7 Goal "is_inf x y (Inf {x, y})";
     5 Goal "is_inf x y (Inf {x, y})";