src/ZF/coinductive.thy
author paulson
Wed, 21 Aug 1996 13:22:23 +0200
changeset 1933 8b24773de6db
parent 124 858ab9a9b047
permissions -rw-r--r--
Addition of message NS5

(*Dummy theory to document dependencies *)

coinductive = "ind_syntax" + "intr_elim"