isabelle: src/ZF/Inductive.thy@5c60e46a07c1 (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	*)
578 efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without lcp parents: diff changeset	7
13356 c9cfe1638bf2 improved presentation markup paulson parents: 13259 diff changeset	8	header{Inductive and Coinductive Definitions}
c9cfe1638bf2 improved presentation markup paulson parents: 13259 diff changeset	9
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 13357 diff changeset	10	theory Inductive imports Fixedpt QPair
9bc16273c2d4 migrated theory headers to new format haftmann parents: 13357 diff changeset	11	uses
12183 c10cea75dd56 adapted primrec/datatype to Isar; wenzelm parents: 12175 diff changeset	12	"ind_syntax.ML"
12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	13	"Tools/cartprod.ML"
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	14	"Tools/ind_cases.ML"
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	15	"Tools/inductive_package.ML"
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	16	"Tools/induct_tacs.ML"
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 13357 diff changeset	17	"Tools/primrec_package.ML" begin
12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	18
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 9491 diff changeset	19	setup IndCases.setup
12208 5efe7b6874fd setup DatatypeTactics.setup; wenzelm parents: 12183 diff changeset	20	setup DatatypeTactics.setup
2870 6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 805 diff changeset	21
6d6fd10a9fdc Now a non-trivial theory so that require_thy can find it paulson parents: 805 diff changeset	22	end

author	wenzelm
	Thu, 04 Jan 2007 19:27:08 +0100
changeset 22002	5c60e46a07c1
parent 16417	9bc16273c2d4
child 22814	4cd25f1706bb
permissions	-rw-r--r--