isabelle: Admin/Benchmarks/HOL-datatype/Brackin.thy@f2a587696afb (annotated)

7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	1	(* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy
33695 bec342db1bf4 eliminated obsolete CVS Ids; wenzelm parents: 16417 diff changeset	2
bec342db1bf4 eliminated obsolete CVS Ids; wenzelm parents: 16417 diff changeset	3	A couple from Steve Brackin's work.
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	4	*)
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	5
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 7373 diff changeset	6	theory Brackin imports Main begin
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	7
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	8	datatype T = X1 \| X2 \| X3 \| X4 \| X5 \| X6 \| X7 \| X8 \| X9 \| X10 \| X11 \|
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	9	X12 \| X13 \| X14 \| X15 \| X16 \| X17 \| X18 \| X19 \| X20 \| X21 \|
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	10	X22 \| X23 \| X24 \| X25 \| X26 \| X27 \| X28 \| X29 \| X30 \| X31 \|
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	11	X32 \| X33 \| X34
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	12
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	13	datatype
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	14	('a, 'b, 'c) TY1 =
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	15	NoF__
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	16	\| Fk__ 'a "('a, 'b, 'c) TY2"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	17	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	18	('a, 'b, 'c) TY2 =
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	19	Ta__ bool
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	20	\| Td__ bool
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	21	\| Tf__ "('a, 'b, 'c) TY1"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	22	\| Tk__ bool
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	23	\| Tp__ bool
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	24	\| App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	25	\| Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	26	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	27	('a, 'b, 'c) TY3 =
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	28	NoS__
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	29	\| Fresh__ "('a, 'b, 'c) TY2"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	30	\| Trustworthy__ 'a
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	31	\| PrivateKey__ 'a 'b 'c
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	32	\| PublicKey__ 'a 'b 'c
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	33	\| Conveyed__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	34	\| Possesses__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	35	\| Received__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	36	\| Recognizes__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	37	\| NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	38	\| Sends__ 'a "('a, 'b, 'c) TY2" 'b
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	39	\| SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	40	\| Believes__ 'a "('a, 'b, 'c) TY3"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	41	\| And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	42
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	43	end

author	wenzelm
	Wed, 23 Nov 2011 22:59:39 +0100
changeset 45620	f2a587696afb
parent 33695	bec342db1bf4
permissions	-rw-r--r--