| changeset 19683 | 3620e494cef2 |
| parent 19656 | 09be06943252 |
| child 19756 | 61c4117345c6 |
| 19682:c8c301eb965a | 19683:3620e494cef2 |
|---|---|
14 subsection {* Syntax and axiomatic basis *} |
14 subsection {* Syntax and axiomatic basis *} |
15 |
15 |
16 global |
16 global |
17 |
17 |
18 classes "term" |
18 classes "term" |
19 finalconsts term_class |
|
20 defaultsort "term" |
19 defaultsort "term" |
21 |
20 |
22 typedecl o |
21 typedecl o |
23 |
22 |
24 judgment |
23 judgment |