equal
deleted
inserted
replaced
32 time_use_thy "Tarski"; |
32 time_use_thy "Tarski"; |
33 |
33 |
34 time_use_thy "StringEx"; |
34 time_use_thy "StringEx"; |
35 time_use_thy "BinEx"; |
35 time_use_thy "BinEx"; |
36 |
36 |
37 if svc_enabled() then time_use_thy "svc_test" |
37 if_svc_enabled time_use_thy "svc_test"; |
38 else (); |
|
39 |
38 |
40 (*basic use of extensible records*) |
39 (*basic use of extensible records*) |
41 time_use_thy "MonoidGroup"; |
40 time_use_thy "MonoidGroup"; |
42 time_use_thy "Points"; |
41 time_use_thy "Points"; |
43 |
42 |