isabelle: src/HOL/Datatype.thy@64bf7da1994a (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	wenzelm
	Sun, 17 Sep 2000 22:19:02 +0200
changeset 10007	64bf7da1994a
parent 5759	bf5d9e5b8cdf
child 10212	33fe2d701ddd
permissions	-rw-r--r--