doc-src/Tutorial/Recdef/sep1
author wenzelm
Mon, 28 Aug 2000 20:28:44 +0200
changeset 9701 533df6cedc2d
parent 6100 40d66bc3e83f
permissions -rw-r--r--
* \isabellestyle{it} produces near math mode output; * settings: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, XSYMBOL_HOME;

recdef sep "measure (%(a,xs). length xs)"
  "sep(a, x#y#zs) = x # a # sep(a,y#zs)"
  "sep(a, xs)     = xs"