equal
deleted
inserted
replaced
7 |
7 |
8 theory IFOLP |
8 theory IFOLP |
9 imports Pure |
9 imports Pure |
10 begin |
10 begin |
11 |
11 |
12 ML_file \<open>~~/src/Tools/simp_legacy.ML\<close> |
|
13 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close> |
12 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close> |
14 |
13 |
15 setup Pure_Thy.old_appl_syntax_setup |
14 setup Pure_Thy.old_appl_syntax_setup |
16 setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close> |
15 setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close> |
17 |
16 |