src/ZF/Inductive.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 13357 6f54e992777e
child 22814 4cd25f1706bb
permissions -rw-r--r--
migrated theory headers to new format
     1 (*  Title:      ZF/Inductive.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 *)
     7 
     8 header{*Inductive and Coinductive Definitions*}
     9 
    10 theory Inductive imports Fixedpt QPair
    11   uses
    12     "ind_syntax.ML"
    13     "Tools/cartprod.ML"
    14     "Tools/ind_cases.ML"
    15     "Tools/inductive_package.ML"
    16     "Tools/induct_tacs.ML"
    17     "Tools/primrec_package.ML" begin
    18 
    19 setup IndCases.setup
    20 setup DatatypeTactics.setup
    21 
    22 end