equal
deleted
inserted
replaced
5 |
5 |
6 header {* Parsing and pretty-printing of sequences *} |
6 header {* Parsing and pretty-printing of sequences *} |
7 |
7 |
8 theory Sequents |
8 theory Sequents |
9 imports Pure |
9 imports Pure |
10 uses ("prover.ML") |
|
11 begin |
10 begin |
12 |
11 |
13 setup Pure_Thy.old_appl_syntax_setup |
12 setup Pure_Thy.old_appl_syntax_setup |
14 |
13 |
15 declare [[unify_trace_bound = 20, unify_search_bound = 40]] |
14 declare [[unify_trace_bound = 20, unify_search_bound = 40]] |
140 fun side_tr [s1] = seq_tr s1; |
139 fun side_tr [s1] = seq_tr s1; |
141 *} |
140 *} |
142 |
141 |
143 parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *} |
142 parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *} |
144 |
143 |
145 use "prover.ML" |
144 ML_file "prover.ML" |
146 |
145 |
147 end |
146 end |
148 |
147 |