src/ZF/add_ind_def.thy
author paulson
Fri, 10 Apr 1998 13:15:28 +0200
changeset 4804 02b7c759159b
parent 1735 96244c247b07
permissions -rw-r--r--
Fixed bug in inductive sections to allow disjunctive premises; added tracing flag trace_induct

(*Dummy theory to document dependencies *)

add_ind_def = Fixedpt + "ind_syntax" + "cartprod"