| changeset 70880 | de2e2382bc0d |
| parent 69593 | 3dda49e08b9d |
| 70879:0b320e92485c | 70880:de2e2382bc0d |
|---|---|
9 section \<open>Classical First-Order Sequent Calculus\<close> |
9 section \<open>Classical First-Order Sequent Calculus\<close> |
10 |
10 |
11 theory LK0 |
11 theory LK0 |
12 imports Sequents |
12 imports Sequents |
13 begin |
13 begin |
14 |
|
15 setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close> |
|
14 |
16 |
15 class "term" |
17 class "term" |
16 default_sort "term" |
18 default_sort "term" |
17 |
19 |
18 consts |
20 consts |