| changeset 70880 | de2e2382bc0d |
| parent 69605 | a96320074298 |
| child 74301 | ffe269e74bdd |
| 70879:0b320e92485c | 70880:de2e2382bc0d |
|---|---|
10 begin |
10 begin |
11 |
11 |
12 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close> |
12 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close> |
13 |
13 |
14 setup Pure_Thy.old_appl_syntax_setup |
14 setup Pure_Thy.old_appl_syntax_setup |
15 setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close> |
|
15 |
16 |
16 class "term" |
17 class "term" |
17 default_sort "term" |
18 default_sort "term" |
18 |
19 |
19 typedecl p |
20 typedecl p |