| changeset 53280 | 36ffe23b25f8 |
| parent 49906 | c0eafbd55de3 |
| child 56570 | 901a6696cdd8 |
| 53279:348aed032cda | 53280:36ffe23b25f8 |
|---|---|
137 (** for the <<...>> notation **) |
137 (** for the <<...>> notation **) |
138 |
138 |
139 fun side_tr [s1] = seq_tr s1; |
139 fun side_tr [s1] = seq_tr s1; |
140 *} |
140 *} |
141 |
141 |
142 parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *} |
142 parse_translation {* [(@{syntax_const "_Side"}, K side_tr)] *} |
143 |
143 |
144 ML_file "prover.ML" |
144 ML_file "prover.ML" |
145 |
145 |
146 end |
146 end |
147 |
147 |