src/ZF/inductive.thy
author wenzelm
Sat, 24 Oct 1998 20:22:45 +0200
changeset 5764 ea464976a00f
parent 124 858ab9a9b047
permissions -rw-r--r--
records; tuned datatype, inductive, primrec;

(*Dummy theory to document dependencies *)

inductive = "indrule"