src/ZF/Inductive.thy
author wenzelm
Wed Nov 14 18:46:30 2001 +0100 (2001-11-14)
changeset 12183 c10cea75dd56
parent 12175 5cf58a1799a7
child 12208 5efe7b6874fd
permissions -rw-r--r--
adapted primrec/datatype to 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@12183
    11
    "ind_syntax.ML"
wenzelm@12175
    12
    "Tools/cartprod.ML"
wenzelm@12175
    13
    "Tools/ind_cases.ML"
wenzelm@12175
    14
    "Tools/inductive_package.ML"
wenzelm@12175
    15
    "Tools/induct_tacs.ML"
wenzelm@12175
    16
    "Tools/primrec_package.ML":
wenzelm@12175
    17
wenzelm@12175
    18
setup IndCases.setup
wenzelm@12175
    19
setup induct_tacs_setup
paulson@2870
    20
paulson@2870
    21
end