isabelle: src/HOL/Datatype.thy@28a53b68a8c0 (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
10212 33fe2d701ddd * empty log message * nipkow parents: 5759 diff changeset	7	Datatype = Datatype_Universe +
5181 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
	Wed, 10 Jan 2001 11:00:17 +0100
changeset 10840	28a53b68a8c0
parent 10212	33fe2d701ddd
child 11954	3d1780208bf3
permissions	-rw-r--r--