equal
deleted
inserted
replaced
1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
1 (* Title: Tools/IsaPlanner/rw_tools.ML |
2 (* Title: Pure/IsaPlanner/rw_tools.ML |
|
3 ID: $Id$ |
2 ID: $Id$ |
4 Author: Lucas Dixon, University of Edinburgh |
3 Author: Lucas Dixon, University of Edinburgh |
5 lucas.dixon@ed.ac.uk |
|
6 Created: 28 May 2004 |
|
7 *) |
|
8 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
9 (* DESCRIPTION: |
|
10 |
4 |
11 term related tools used for rewriting |
5 Term related tools used for rewriting. |
12 |
|
13 *) |
6 *) |
14 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
15 |
7 |
16 signature RWTOOLS = |
8 signature RWTOOLS = |
17 sig |
9 sig |
18 end; |
10 end; |
19 |
11 |