| changeset 16179 | fa7e70be26b0 |
| parent 15574 | b1d1b5bfc464 |
| child 18921 | f47c46d7d654 |
| 16178:754efc5afd5d | 16179:fa7e70be26b0 |
|---|---|
1 (* Title: search |
1 (* Title: Pure/search.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson and Norbert Voelker |
3 Author: Lawrence C Paulson and Norbert Voelker |
4 |
4 |
5 Search tacticals |
5 Search tacticals. |
6 *) |
6 *) |
7 |
7 |
8 infix 1 THEN_MAYBE THEN_MAYBE'; |
8 infix 1 THEN_MAYBE THEN_MAYBE'; |
9 |
9 |
10 signature SEARCH = |
10 signature SEARCH = |