equal
deleted
inserted
replaced
1 (* Title: HOL/AxClasses/Tutorial/ROOT.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
1 |
5 Some simple axclass demos that go along with the paper "Using |
|
6 Axiomatic Type Classes in Isabelle --- a tutorial". (The NatClass |
|
7 example resides in directory FOL/ex/.) |
|
8 *) |
|
9 |
|
10 set show_types; |
|
11 set show_sorts; |
|
12 |
|
13 |
|
14 (* Semigroups *) |
|
15 |
|
16 use_thy "Semigroup"; |
|
17 use_thy "Semigroups"; |
2 use_thy "Semigroups"; |
18 |
|
19 |
|
20 (* Basic group theory *) |
|
21 |
|
22 use_thy "Sigs"; |
|
23 use_thy "Monoid"; |
|
24 use_thy "Group"; |
3 use_thy "Group"; |
25 use_thy "MonoidGroupInsts"; |
|
26 use_thy "Xor"; |
|
27 use_thy "BoolGroupInsts"; |
|
28 use_thy "ProdGroupInsts"; |
|
29 |
|
30 |
|
31 (* Syntactic classes *) |
|
32 |
|
33 use_thy "Product"; |
4 use_thy "Product"; |
34 use_thy "ProductInsts"; |
|