isabelle: Admin/Benchmarks/HOL-datatype/SML.thy@ab01b72715ef (annotated)

7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	1	(* Title: Admin/Benchmarks/HOL-datatype/SML.thy
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	2	ID: $Id$
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	3	*)
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	4
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 7373 diff changeset	5	theory SML imports Main begin
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	6
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	(* Example from Myra: part of the syntax of SML. *)
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	9	(* ------------------------------------------------------------------------- *)
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	string = EMPTY_STRING \| CONS_STRING nat 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	strid = STRID 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	var = VAR 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	con = CON 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	scon = SCINT nat \| SCSTR 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	excon = EXCON 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
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	30	label = LABEL string
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 nonemptylist = Head_and_tail 'a "'a list"
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
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	36	'a long = BASE 'a \| QUALIFIED strid "'a long"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	37
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	38	datatype
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	39	atpat_e = WILDCARDatpat_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	40	\| SCONatpat_e scon
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	41	\| VARatpat_e var
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	42	\| CONatpat_e "con long"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	43	\| EXCONatpat_e "excon long"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	44	\| RECORDatpat_e "patrow_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	45	\| PARatpat_e pat_e
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	patrow_e = DOTDOTDOT_e
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	48	\| PATROW_e label pat_e "patrow_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	49	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	50	pat_e = ATPATpat_e atpat_e
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	51	\| CONpat_e "con long" atpat_e
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	52	\| EXCONpat_e "excon long" atpat_e
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	53	\| LAYEREDpat_e var pat_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	54	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	55	conbind_e = CONBIND_e con "conbind_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	56	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	57	datbind_e = DATBIND_e conbind_e "datbind_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	58	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	59	exbind_e = EXBIND1_e excon "exbind_e option"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	60	\| EXBIND2_e excon "excon long" "exbind_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	61	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	62	atexp_e = SCONatexp_e scon
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	63	\| VARatexp_e "var long"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	64	\| CONatexp_e "con long"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	65	\| EXCONatexp_e "excon long"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	66	\| RECORDatexp_e "exprow_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	67	\| LETatexp_e dec_e exp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	68	\| PARatexp_e exp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	69	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	70	exprow_e = EXPROW_e label exp_e "exprow_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	71	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	72	exp_e = ATEXPexp_e atexp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	73	\| APPexp_e exp_e atexp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	74	\| HANDLEexp_e exp_e match_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	75	\| RAISEexp_e exp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	76	\| FNexp_e match_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	77	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	78	match_e = MATCH_e mrule_e "match_e option"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	79	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	80	mrule_e = MRULE_e pat_e exp_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	81	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	82	dec_e = VALdec_e valbind_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	83	\| DATATYPEdec_e datbind_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	84	\| ABSTYPEdec_e datbind_e dec_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	85	\| EXCEPTdec_e exbind_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	86	\| LOCALdec_e dec_e dec_e
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	87	\| OPENdec_e "strid long nonemptylist"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	88	\| EMPTYdec_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	89	\| SEQdec_e dec_e dec_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	90	and
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	91	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	92	\| RECvalbind_e valbind_e
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	93
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	94	end

author	blanchet
	Wed, 28 Oct 2009 17:43:43 +0100
changeset 33561	ab01b72715ef
parent 16417	9bc16273c2d4
child 33695	bec342db1bf4
permissions	-rw-r--r--