src/ZF/Inductive.thy
author wenzelm
Wed, 14 Sep 1994 16:11:19 +0200
changeset 613 f9eb0f819642
parent 578 efc648d29dd0
child 805 96f51689cdeb
permissions -rw-r--r--
removed lookup_const (use Sign.const_type instead);

(*Dummy theory to document dependencies *)

Inductive = "indrule"