| changeset 74158 | 1cb0ad6f9a2d |
| parent 74147 | d030b988d470 |
| child 74210 | c14774713d62 |
| 74156:ecf80e37ed1a | 74158:1cb0ad6f9a2d |
|---|---|
1 (* Title: Pure/System/bash.ML |
1 (* Title: Pure/System/bash.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Syntax for GNU bash. |
4 Support for GNU bash. |
5 *) |
5 *) |
6 |
6 |
7 signature BASH = |
7 signature BASH = |
8 sig |
8 sig |
9 val string: string -> string |
9 val string: string -> string |