| changeset 70880 | de2e2382bc0d |
| parent 70432 | 495881aadbff |
| child 71839 | 0bbe0866b7e6 |
| 70879:0b320e92485c | 70880:de2e2382bc0d |
|---|---|
21 |
21 |
22 |
22 |
23 subsection \<open>Syntax and axiomatic basis\<close> |
23 subsection \<open>Syntax and axiomatic basis\<close> |
24 |
24 |
25 setup Pure_Thy.old_appl_syntax_setup |
25 setup Pure_Thy.old_appl_syntax_setup |
26 setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close> |
|
26 |
27 |
27 class "term" |
28 class "term" |
28 default_sort \<open>term\<close> |
29 default_sort \<open>term\<close> |
29 |
30 |
30 typedecl o |
31 typedecl o |