| changeset 18523 | 9446cb8e1f65 |
| parent 18481 | b75ce99617c7 |
| child 18708 | 4b3dadb4fe33 |
| 18522:9bdfb6eaf8ab | 18523:9446cb8e1f65 |
|---|---|
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 final_consts term_class |
19 finalconsts term_class |
20 defaultsort "term" |
20 defaultsort "term" |
21 |
21 |
22 typedecl o |
22 typedecl o |
23 |
23 |
24 judgment |
24 judgment |