isabelle: src/HOL/Datatype.thy@38f96394c099 (annotated)

5181 4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	1	(* Title: HOL/Datatype.thy
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	2	ID: $Id$
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	3	Author: Stefan Berghofer
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	4	Copyright 1998 TU Muenchen
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	5	*)
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	6
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	7	Datatype = Univ +
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	8
5759 bf5d9e5b8cdf unit and bool are now represented as datatypes. berghofe parents: 5714 diff changeset	9	rep_datatype bool
bf5d9e5b8cdf unit and bool are now represented as datatypes. berghofe parents: 5714 diff changeset	10	distinct True_not_False, False_not_True
bf5d9e5b8cdf unit and bool are now represented as datatypes. berghofe parents: 5714 diff changeset	11	induct bool_induct
bf5d9e5b8cdf unit and bool are now represented as datatypes. berghofe parents: 5714 diff changeset	12
5181 4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	13	rep_datatype sum
5714 b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5181 diff changeset	14	distinct Inl_not_Inr, Inr_not_Inl
b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5181 diff changeset	15	inject Inl_eq, Inr_eq
5181 4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	16	induct sum_induct
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	17
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	18	rep_datatype prod
5714 b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5181 diff changeset	19	inject Pair_eq
b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5181 diff changeset	20	induct prod_induct
5181 4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	21
5759 bf5d9e5b8cdf unit and bool are now represented as datatypes. berghofe parents: 5714 diff changeset	22	rep_datatype unit
bf5d9e5b8cdf unit and bool are now represented as datatypes. berghofe parents: 5714 diff changeset	23	induct unit_induct
bf5d9e5b8cdf unit and bool are now represented as datatypes. berghofe parents: 5714 diff changeset	24
5181 4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	25	end

author	paulson
	Fri, 18 Feb 2000 15:35:29 +0100
changeset 8255	38f96394c099
parent 5759	bf5d9e5b8cdf
child 10212	33fe2d701ddd
permissions	-rw-r--r--