equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Sugar |
2 theory Sugar |
3 imports LaTeXsugar OptionalSugar |
3 imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar" |
4 begin |
4 begin |
5 (*>*) |
5 (*>*) |
6 |
6 |
7 section "Introduction" |
7 section "Introduction" |
8 |
8 |