changeset 74334 | ead56ad40e15 |
parent 73761 | ef1a18e20ace |
child 74658 | 4c508826fee8 |
--- a/src/Doc/Main/Main_Doc.thy Mon Sep 20 23:15:02 2021 +0200 +++ b/src/Doc/Main/Main_Doc.thy Tue Sep 21 00:20:47 2021 +0200 @@ -89,7 +89,7 @@ \subsubsection*{Syntax} -Available by loading theory \<open>Lattice_Syntax\<close> in directory \<open>Library\<close>. +Available via \<^theory_text>\<open>unbundle lattice_syntax\<close>. \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} @{text[source]"x \<sqsubseteq> y"} & \<^term>\<open>x \<le> y\<close>\\