isabelle: src/HOL/Datatype_Benchmark/SML.thy@93eda35a8377 (annotated)

45860 93eda35a8377 more visible benchmarks; wenzelm parents: 33695 diff changeset	1	(* Title: HOL/Datatype_Benchmark/SML.thy
33695 bec342db1bf4 eliminated obsolete CVS Ids; wenzelm parents: 16417 diff changeset	2
bec342db1bf4 eliminated obsolete CVS Ids; wenzelm parents: 16417 diff changeset	3	Example from Myra: part of the syntax of SML.
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 SML 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
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	9	string = EMPTY_STRING \| CONS_STRING nat string
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	10
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	11	datatype
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	12	strid = STRID string
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	13
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	14	datatype
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	15	var = VAR string
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	16
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	17	datatype
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	18	con = CON string
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	19
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	20	datatype
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	21	scon = SCINT nat \| SCSTR string
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	22
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	23	datatype
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	24	excon = EXCON string
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	25
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	26	datatype
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	27	label = LABEL string
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	28
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	29	datatype
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	30	'a nonemptylist = Head_and_tail 'a "'a list"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	31
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	32	datatype
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	33	'a long = BASE 'a \| QUALIFIED strid "'a long"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	34
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	35	datatype
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	36	atpat_e = WILDCARDatpat_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	37	\| SCONatpat_e scon
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	38	\| VARatpat_e var
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	39	\| CONatpat_e "con long"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	40	\| EXCONatpat_e "excon long"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	41	\| RECORDatpat_e "patrow_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	42	\| PARatpat_e pat_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	43	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	44	patrow_e = DOTDOTDOT_e
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	45	\| PATROW_e label pat_e "patrow_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	46	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	47	pat_e = ATPATpat_e atpat_e
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	48	\| CONpat_e "con long" atpat_e
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	49	\| EXCONpat_e "excon long" atpat_e
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	50	\| LAYEREDpat_e var pat_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	51	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	52	conbind_e = CONBIND_e con "conbind_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	53	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	54	datbind_e = DATBIND_e conbind_e "datbind_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	55	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	56	exbind_e = EXBIND1_e excon "exbind_e option"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	57	\| EXBIND2_e excon "excon long" "exbind_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	58	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	59	atexp_e = SCONatexp_e scon
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	60	\| VARatexp_e "var long"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	61	\| CONatexp_e "con long"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	62	\| EXCONatexp_e "excon long"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	63	\| RECORDatexp_e "exprow_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	64	\| LETatexp_e dec_e exp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	65	\| PARatexp_e exp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	66	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	67	exprow_e = EXPROW_e label exp_e "exprow_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	68	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	69	exp_e = ATEXPexp_e atexp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	70	\| APPexp_e exp_e atexp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	71	\| HANDLEexp_e exp_e match_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	72	\| RAISEexp_e exp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	73	\| FNexp_e match_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	74	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	75	match_e = MATCH_e mrule_e "match_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	76	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	77	mrule_e = MRULE_e pat_e exp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	78	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	79	dec_e = VALdec_e valbind_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	80	\| DATATYPEdec_e datbind_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	81	\| ABSTYPEdec_e datbind_e dec_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	82	\| EXCEPTdec_e exbind_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	83	\| LOCALdec_e dec_e dec_e
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	84	\| OPENdec_e "strid long nonemptylist"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	85	\| EMPTYdec_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	86	\| SEQdec_e dec_e dec_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	87	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	88	valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	89	\| RECvalbind_e valbind_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	90
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	91	end

author	wenzelm
	Wed, 14 Dec 2011 12:02:02 +0100
changeset 45860	93eda35a8377
parent 33695	Admin/Benchmarks/HOL-datatype/SML.thy@bec342db1bf4
permissions	-rw-r--r--