src/ZF/coinductive.thy
author wenzelm
Tue, 28 Oct 1997 17:36:16 +0100
changeset 4022 0770a19c48d3
parent 124 858ab9a9b047
permissions -rw-r--r--
added ignored_consts, thms_containing, add_store_axioms(_i), add_store_defs(_i), thms_of; tuned pure thys;

(*Dummy theory to document dependencies *)

coinductive = "ind_syntax" + "intr_elim"