README
1+ ===================================================================== +
2| |
3| LIBRARY : string |
4| |
5| DESCRIPTION : definition of logical types for characters and |
6| and strings of characters. |
7| |
8| AUTHOR : K. Slind |
9| DATE : 11.02.01 |
10| ===================================================================== +
11
12
13+ --------------------------------------------------------------------- +
14| |
15| FILES: |
16| |
17+ --------------------------------------------------------------------- +
18
19 stringLib.{sig,sml} Load all string functionality. Includes
20 conversions for character equality,
21 and string equality, as well as a conversion
22 for proving instances of
23
24 ORD (CHAR m) = m
25
26
27 stringScript.sml Creates the theory of character strings
28
29 stringSyntax.{sig,sml} Derived syntax operations for characters
30 and strings.
31
32 stringSimps.sml Simplification set for strings, to be used
33 by simpLib rewriters (also found in bossLib).
34
35+ --------------------------------------------------------------------- +
36| |
37| TO REBUILD THE LIBRARY: |
38| |
39+ --------------------------------------------------------------------- +
40
41 1) invoke "Holmake" as a shell command
42
43
44+ --------------------------------------------------------------------- +
45| |
46| TO USE THE LIBRARY: |
47| |
48+ --------------------------------------------------------------------- +
49
50 1) type
51
52 load "stringLib";
53
54 into an interactive session of HOL.
55