\begin{lisp:documentation}{*examples*}{VARIABLE}{'((string$-$grobner (string$-$grobner [x\symbol{94}2+y,x$-$y] '(x y)) (string$-$grobner [y$-$x\symbol{94}2,z$-$x\symbol{94}3] '(x y z) order \#'grevlex$>$))
 (string$-$grobner$-$system (string$-$grobner$-$system [u*x+y,x+y] '(x y) '(u)) (string$-$grobner$-$system [u*x+y,x+y] '(x y) '(u) cover '(([u$-$1] [])))) (string$-$read$-$poly (string$-$read$-$poly [x\symbol{94}3+3*x\symbol{94}2+3*x+1] '(x)))
 (string$-$elimination$-$ideal (string$-$elimination$-$ideal [x\symbol{94}2+y\symbol{94}2$-$2,x*y$-$1] '(x y) 1)) (string$-$ideal$-$saturation$-$1 (string$-$ideal$-$saturation$-$1 [x\symbol{94}2*y,y\symbol{94}3] x '(x y)))
 (string$-$ideal$-$polysaturation$-$1 (string$-$ideal$-$polysaturation$-$1 [x\symbol{94}2*y,y\symbol{94}3] [x,y] '(x y))) (string$-$cond (string$-$cond '([u\symbol{94}2$-$v] [v$-$1]) '(u v) \#'grevlex$>$))
 (string$-$cover (string$-$cover '(([u\symbol{94}2$-$v] [u]) ([u+v] [])) '(u v) \#'grevlex$>$)) (string$-$determine (string$-$determine [u*x+y,v*x\symbol{94}2+y\symbol{94}2] '(x y) '(u v) cond '([u,v] [v$-$1]) main$-$order \#'lex$>$))
 (parse$-$string$-$to$-$sorted$-$alist (parse$-$string$-$to$-$sorted$-$alist x\symbol{94}2+y\symbol{94}3 '(x y) \#'grevlex$>$) (parse$-$string$-$to$-$sorted$-$alist [x\symbol{94}2+y\symbol{94}3,x$-$y] '(x y) \#'grevlex$>$))
 (translate$-$statements (translate$-$statements (collinear a b c) (perpendicular a b a c)))
 (translate$-$theorem (translate$-$theorem ((perpendicular a b c d) (perpendicular c d e f)) ((parallel a b e f) (identical$-$points c d)))
  (translate$-$theorem ((perpendicular a b a c) (midpoint b c m) (midpoint a m o) (collinear b h c) (perpendicular a h b c)) ((equidistant m o h o) (identical$-$points b c))))
 (prove$-$theorem (prove$-$theorem ((perpendicular a b c d) (perpendicular c d e f)) ((parallel a b e f) (identical$-$points c d)))
  (prove$-$theorem ((perpendicular a b a c) (midpoint b c m) (midpoint a m o) (collinear b h c) (perpendicular a h b c)) ((equidistant m o h o) (identical$-$points b c)))
  (prove$-$theorem ((perpendicular a b a c) (identical$-$points b c)) ((identical$-$points a b) (identical$-$points a c)))
  (prove$-$theorem ((perpendicular a b a c) (identical$-$points b c)) ((identical$-$points a b) (real$-$identical$-$points a c))))) }
A list of available examples.
\end{lisp:documentation}

\begin{lisp:documentation}{example}{FUNCTION}{symbol {\sf \&optional} (stream t) }
Run short examples associated with a symbol, which typically is a
function name. 
\end{lisp:documentation}

\begin{lisp:documentation}{run$-$example}{FUNCTION}{e stream }
Evaluate a single form E and send output to stream STREAM.
\end{lisp:documentation}

\begin{lisp:documentation}{all$-$examples}{FUNCTION}{{\sf \&optional} (stream t) }
Run all available examples and send output to STREAM.
\end{lisp:documentation}