Command abbreviations:

(* Standard abbreviations *)
(* users are encouraged to propose new abbreviations! *)
val a = axiom;
val s = start;
val wb = workback;
val ri = ruleintro;
val rri = revruleintro;
val ari = altruleintro;
val arri = altrevruleintro;
val ex = execute;
val td = thmdisplay;
val dpt = declarepretheorem;
val dupt = declareunarypretheorem;
val p = prove;
val smt = showmatchtheorem;
val tri = targetruleintro;
val ae = autoedit;
val rp = reprove;
val sat = showalltheorems;
val srt = showrelevantthms;
val dti = defaulttypeinfo;
val nti = notypeinfo;
(* new on July 13, 1999 *)
val ut = upto;
val dtl = downtoleft;
val dtr = downtoright;
val lut = litupto;
val ldtl = litdowntoleft;
val ldtr = litdowntoright;
val mtri = matchtri;
val amtri = anothermatchtri;