src/ZF/add_ind_def.thy
author sandnerr
Mon, 09 Dec 1996 19:13:13 +0100
changeset 2355 ee9bdbe2ac8a
parent 1735 96244c247b07
permissions -rw-r--r--
simpset extension moved from HOLCF.ML to One.ML and Tr2.ML

(*Dummy theory to document dependencies *)

add_ind_def = Fixedpt + "ind_syntax" + "cartprod"