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
wenzelm@12175
     1
(*  Title:      ZF/Inductive.thy
wenzelm@12175
     2
    ID:         $Id$
wenzelm@12175
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@12175
     4
    Copyright   1993  University of Cambridge
wenzelm@12175
     5
wenzelm@12175
     6
*)
lcp@578
     7
paulson@13356
     8
header{*Inductive and Coinductive Definitions*}
paulson@13356
     9
haftmann@16417
    10
theory Inductive imports Fixedpt QPair
haftmann@16417
    11
  uses
wenzelm@12183
    12
    "ind_syntax.ML"
wenzelm@12175
    13
    "Tools/cartprod.ML"
wenzelm@12175
    14
    "Tools/ind_cases.ML"
wenzelm@12175
    15
    "Tools/inductive_package.ML"
wenzelm@12175
    16
    "Tools/induct_tacs.ML"
haftmann@16417
    17
    "Tools/primrec_package.ML" begin
wenzelm@12175
    18
wenzelm@12175
    19
setup IndCases.setup
wenzelm@12208
    20
setup DatatypeTactics.setup
paulson@2870
    21
paulson@2870
    22
end