isabelle: src/ZF/Inductive.thy@5cf58a1799a7 (annotated)

12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	1	(* Title: ZF/Inductive.thy
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	2	ID: $Id$
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	4	Copyright 1993 University of Cambridge
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	5
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	6	(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory.
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	7	*)
578 efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without lcp parents: diff changeset	8
12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	9	theory Inductive = Fixedpt + mono
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	10	files
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	11	"Tools/cartprod.ML"
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	12	"Tools/ind_cases.ML"
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	13	"Tools/inductive_package.ML"
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	14	"Tools/induct_tacs.ML"
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	15	"Tools/primrec_package.ML":
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	16
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	17	setup IndCases.setup
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	18	setup induct_tacs_setup
2870 6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 805 diff changeset	19
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 805 diff changeset	20	end

author	wenzelm
	Tue, 13 Nov 2001 22:20:51 +0100
changeset 12175	5cf58a1799a7
parent 9491	1a36151ee2fc
child 12183	c10cea75dd56
permissions	-rw-r--r--