src/ZF/coinductive.thy
author oheimb
Tue, 04 Nov 1997 14:40:29 +0100
changeset 4122 f63c283cefaf
parent 124 858ab9a9b047
permissions -rw-r--r--
* removed "axioms" and "generated by" section * replaced "ops" section by extended "consts" section, which is capable of handling the continuous function space "->" directly * domain package: now uses normal mixfix annotations (instead of cinfix...)

(*Dummy theory to document dependencies *)

coinductive = "ind_syntax" + "intr_elim"