src/ZF/mono.thy
author wenzelm
Wed, 31 Oct 2001 01:21:01 +0100
changeset 11990 c1daefc08eff
parent 5325 f7a5e06adea1
child 13259 01fa0c8dbc92
permissions -rw-r--r--
use induct_rulify2;

mono = QPair + Sum + func