doc-src/Tutorial/Recdef/sep1prolog
author wenzelm
Tue, 27 Apr 1999 15:10:36 +0200
changeset 6526 6b64d1454ee3
parent 6100 40d66bc3e83f
permissions -rw-r--r--
added Isar_examples/NatSum.thy;

Sep1 = Main +
consts sep :: "'a * 'a list => 'a list"