src/Doc/Locales/Examples3.thy
changeset 63724 e7df93d4d9b8
parent 63680 6e1e8b5abbfa
child 67398 5eb932e604a2
     1.1 --- a/src/Doc/Locales/Examples3.thy	Thu Aug 25 20:08:40 2016 +0200
     1.2 +++ b/src/Doc/Locales/Examples3.thy	Thu Aug 25 20:08:41 2016 +0200
     1.3 @@ -91,8 +91,8 @@
     1.4  \begin{tabular}{l}
     1.5    @{thm [source] int.less_def} from locale @{text partial_order}: \\
     1.6    \quad @{thm int.less_def} \\
     1.7 -  @{thm [source] int.ex_sup} from locale @{text lattice}: \\
     1.8 -  \quad @{thm int.ex_sup} \\
     1.9 +  @{thm [source] int.meet_left} from locale @{text lattice}: \\
    1.10 +  \quad @{thm int.meet_left} \\
    1.11    @{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\
    1.12    \quad @{thm int.join_distr} \\
    1.13    @{thm [source] int.less_total} from locale @{text total_order}: \\