These are abbreviations for names of commonly used commands found below.
(* /////////// ml declarations to change the names of commands //////////// *) fun ri x = ruleintro x; fun rri x = revruleintro x; fun ari x = altruleintro x; fun arri x = altrevruleintro x; fun s x = start x; fun p x = prove x; fun rp x = reprove x; fun ex() = execute(); fun di x = declareinfix x; fun du x = declareunary x; fun a x = axiom x; fun dpt x = declarepretheorem x; fun sp x n = setprecedence x n; fun td x = thmdisplay x; fun wb() = workback(); fun ae x = autoedit x; fun tri x = targetruleintro x; fun smt x = showmatchthm x; fun srt() = showrelevantthms(); fun dti s t = declaretypeinfo s t; fun uti s = detypeinfo s; fun sat() = showalltheorems();