author | nipkow |
Sun, 05 Jan 2003 21:03:14 +0100 | |
changeset 13771 | 6cd59cc885a1 |
parent 13357 | 6f54e992777e |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
(* Title: ZF/Inductive.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge *) header{*Inductive and Coinductive Definitions*} theory Inductive = Fixedpt + QPair files "ind_syntax.ML" "Tools/cartprod.ML" "Tools/ind_cases.ML" "Tools/inductive_package.ML" "Tools/induct_tacs.ML" "Tools/primrec_package.ML": setup IndCases.setup setup DatatypeTactics.setup end