equal
deleted
inserted
replaced
80 latter in theory @{theory Set}). |
80 latter in theory @{theory Set}). |
81 |
81 |
82 \begin{tabular}{@ {} l @ {~::~} l @ {}} |
82 \begin{tabular}{@ {} l @ {~::~} l @ {}} |
83 @{const Lattices.inf} & @{typeof Lattices.inf}\\ |
83 @{const Lattices.inf} & @{typeof Lattices.inf}\\ |
84 @{const Lattices.sup} & @{typeof Lattices.sup}\\ |
84 @{const Lattices.sup} & @{typeof Lattices.sup}\\ |
85 @{const Complete_Lattice.Inf} & @{term_type_only Complete_Lattice.Inf "'a set \<Rightarrow> 'a::Inf"}\\ |
85 @{const Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \<Rightarrow> 'a::Inf"}\\ |
86 @{const Complete_Lattice.Sup} & @{term_type_only Complete_Lattice.Sup "'a set \<Rightarrow> 'a::Sup"}\\ |
86 @{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \<Rightarrow> 'a::Sup"}\\ |
87 \end{tabular} |
87 \end{tabular} |
88 |
88 |
89 \subsubsection*{Syntax} |
89 \subsubsection*{Syntax} |
90 |
90 |
91 Available by loading theory @{text Lattice_Syntax} in directory @{text |
91 Available by loading theory @{text Lattice_Syntax} in directory @{text |