README
1This example defines the abstract syntax for a simple ML-like language,
2and a simple mutually-recursive function for computing the variables of
3an expression of that language. It exercises the new type
4definition package for mutually recursive concrete types.
5
6 The example is also a demonstration of how Holmake works. Just invoke
7
8 Holmake
9
10on the Unix command line and wait. When Holmake is done, a compiled
11theory corresponding to this file is found in MLTheory.u{i,o}. It
12can be loaded into an interactive session by
13
14 load"MLTheory";
15
16Loading the compiled theory can take a little while. Building the theory
17in the first place also takes some time.
18
19 If you are working interactively, i.e., you don't want to pay any
20attention to this Holmake stuff, do the following in an invocation of
21Hol98:
22
23 app load ["Datatype", "stringTheory", "setTheory"];
24
25and then proceed with cut-and-paste from the file MLScript.sml.
26