| changeset 17702 | ea88ddeafabe |
| parent 17591 | 33d409318266 |
| child 18481 | b75ce99617c7 |
| 17701:6928771d256e | 17702:ea88ddeafabe |
|---|---|
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 defaultsort "term" |
20 defaultsort "term" |
20 |
21 |
21 typedecl o |
22 typedecl o |
22 |
23 |
23 judgment |
24 judgment |