(* file ~/public_html/cse773/README.txt, L. Morris, 1/8/03 *)

This subdirectory of my public_html is intended to make relevant textual
material which I have written, and may want to revise from time to time,
accessible to students in CSE 773, Spring 2003 (and to Prof. Stabler).

All the files here (with the exception of the ante_allTacs "Description"
are intended to be plain ASCII; I am giving them the extension .txt in case
that makes them more assimilable to those browsing via a Microsoft product.

Compilable and compiled HOL files for the course, with extensions .sml,
.sig, .uo, .ui, are in the directory /home/ecefac/cse773.

Some more exotic routines additional to ante_allTacs are also in
/home/ecefac/cse773 under the name ante_appTacs.sml and .sig; these
unfortunately have no separate documentation. The likeliest reason for one
to want to load ante_appTacs is for one little abbreviatory function,
"tty", for "toggle types [printing]". If ante_appTacs is open, executing

tty ();

in HOL has the same effect as

showtypes := true;

if showtypes was false, and as

showtypes := false;

if showtypes was true.

(* Instructions to myself: to make any new fooScript.sml file in
  /home/ecefac/cse773  available on the course web page, without copying:

cd to ~/public_html/cse773 (where this README file is) and execute

ln -s /home/ecefac/cse773/fooScript.sml fooScript.sml.txt

and then edit ~/public_html/html/index_cse773.html with a suitable link.