isabelle: src/HOL/Datatype.thy@b4f2e281a907 (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
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	9	rep_datatype sum
5714 b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5181 diff changeset	10	distinct Inl_not_Inr, Inr_not_Inl
b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5181 diff changeset	11	inject Inl_eq, Inr_eq
5181 4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	12	induct sum_induct
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	13
4ba3787d9709 New theory Datatype. Needed as an ancestor when defining datatypes. berghofe parents: diff changeset	14	rep_datatype prod
5714 b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5181 diff changeset	15	inject Pair_eq
b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5181 diff changeset	16	induct prod_induct
5181 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	end

author	berghofe
	Wed, 21 Oct 1998 17:38:47 +0200
changeset 5714	b4f2e281a907
parent 5181	4ba3787d9709
child 5759	bf5d9e5b8cdf
permissions	-rw-r--r--