equal
deleted
inserted
replaced
1 (*<*) |
1 (* $Id$ *) |
|
2 |
2 theory Examples |
3 theory Examples |
3 imports GCD |
4 imports GCD |
4 begin |
5 begin |
5 |
6 |
6 hide const Lattices.lattice |
7 hide %invisible const Lattices.lattice |
7 pretty_setmargin 65 |
8 pretty_setmargin %invisible 65 |
8 |
|
9 (*>*) |
|
10 |
9 |
11 (* |
10 (* |
12 text {* The following presentation will use notation of |
11 text {* The following presentation will use notation of |
13 Isabelle's meta logic, hence a few sentences to explain this. |
12 Isabelle's meta logic, hence a few sentences to explain this. |
14 The logical |
13 The logical |
676 qed |
675 qed |
677 qed |
676 qed |
678 |
677 |
679 text {* The locale hierarchy is now as shown in Figure~\ref{fig:lattices}(c). *} |
678 text {* The locale hierarchy is now as shown in Figure~\ref{fig:lattices}(c). *} |
680 |
679 |
681 (*<*) |
|
682 end |
680 end |
683 (*>*) |
|