equal
deleted
inserted
replaced
1 |
1 |
2 \documentclass[12pt,a4paper,fleqn]{report} |
2 \documentclass[12pt,a4paper,fleqn]{article} |
3 \usepackage{latexsym,graphicx} |
3 \usepackage{latexsym,graphicx} |
4 \usepackage[refpage]{nomencl} |
4 \usepackage[refpage]{nomencl} |
5 \usepackage{../iman,../extra,../isar,../proof} |
5 \usepackage{../iman,../extra,../isar,../proof} |
6 \usepackage{../isabelle,../isabellesym} |
6 \usepackage{../isabelle,../isabellesym} |
7 \usepackage{style} |
7 \usepackage{style} |
19 \begin{document} |
19 \begin{document} |
20 |
20 |
21 \maketitle |
21 \maketitle |
22 |
22 |
23 \begin{abstract} |
23 \begin{abstract} |
24 This tutorial introduces the look-and-feel of Isar type classes |
24 \noindent This tutorial introduces the look-and-feel of Isar type classes |
25 to the end-user; Isar type classes are a convenient mechanism |
25 to the end-user; Isar type classes are a convenient mechanism |
26 for organizing specifications, overcoming some drawbacks |
26 for organizing specifications, overcoming some drawbacks |
27 of raw axiomatic type classes. Essentially, they combine |
27 of raw axiomatic type classes. Essentially, they combine |
28 an operational aspect (in the manner of Haskell) with |
28 an operational aspect (in the manner of Haskell) with |
29 a logical aspect, both managed uniformly. |
29 a logical aspect, both managed uniformly. |