src/ZF/Inductive.thy
author wenzelm
Tue Nov 13 22:20:51 2001 +0100 (2001-11-13)
changeset 12175 5cf58a1799a7
parent 9491 1a36151ee2fc
child 12183 c10cea75dd56
permissions -rw-r--r--
rearranged inductive package for Isar;
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
(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory.
wenzelm@12175
     7
*)
lcp@578
     8
wenzelm@12175
     9
theory Inductive = Fixedpt + mono
wenzelm@12175
    10
  files
wenzelm@12175
    11
    "Tools/cartprod.ML"
wenzelm@12175
    12
    "Tools/ind_cases.ML"
wenzelm@12175
    13
    "Tools/inductive_package.ML"
wenzelm@12175
    14
    "Tools/induct_tacs.ML"
wenzelm@12175
    15
    "Tools/primrec_package.ML":
wenzelm@12175
    16
wenzelm@12175
    17
setup IndCases.setup
wenzelm@12175
    18
setup induct_tacs_setup
paulson@2870
    19
paulson@2870
    20
end